Metamath Proof Explorer
Table of Contents - 10.4.1. Definition and basic properties
- cdr
- cfield
- df-drng
- df-field
- isdrng
- drngunit
- drngui
- drngring
- drnggrp
- isfld
- isdrng2
- drngprop
- drngmgp
- drngmcl
- drngid
- drngunz
- drngid2
- drnginvrcl
- drnginvrn0
- drnginvrl
- drnginvrr
- drngmul0or
- drngmulne0
- drngmuleq0
- opprdrng
- isdrngd
- isdrngrd
- drngpropd
- fldpropd