Metamath Proof Explorer

Table of Contents - 10.4. Division rings and fields

1. Definition and basic properties
   1. cdr
   2. cfield
   3. df-drng
   4. df-field
   5. isdrng
   6. drngunit
   7. drngui
   8. drngring
   9. drnggrp
   10. isfld
   11. isdrng2
   12. drngprop
   13. drngmgp
   14. drngmcl
   15. drngid
   16. drngunz
   17. drngid2
   18. drnginvrcl
   19. drnginvrn0
   20. drnginvrl
   21. drnginvrr
   22. drngmul0or
   23. drngmulne0
   24. drngmuleq0
   25. opprdrng
   26. isdrngd
   27. isdrngrd
   28. drngpropd
   29. fldpropd
2. Subrings of a ring
   1. csubrg
   2. crgspn
   3. df-subrg
   4. df-rgspn
   5. issubrg
   6. subrgss
   7. subrgid
   8. subrgring
   9. subrgcrng
   10. subrgrcl
   11. subrgsubg
   12. subrg0
   13. subrg1cl
   14. subrgbas
   15. subrg1
   16. subrgacl
   17. subrgmcl
   18. subrgsubm
   19. subrgdvds
   20. subrguss
   21. subrginv
   22. subrgdv
   23. subrgunit
   24. subrgugrp
   25. issubrg2
   26. opprsubrg
   27. subrgint
   28. subrgin
   29. subrgmre
   30. issubdrg
   31. subsubrg
   32. subsubrg2
   33. issubrg3
   34. resrhm
   35. rhmeql
   36. rhmima
   37. rnrhmsubrg
   38. cntzsubr
   39. pwsdiagrhm
   40. subrgpropd
   41. rhmpropd
   42. Sub-division rings
3. Absolute value (abstract algebra)
   1. cabv
   2. df-abv
   3. abvfval
   4. isabv
   5. isabvd
   6. abvrcl
   7. abvfge0
   8. abvf
   9. abvcl
   10. abvge0
   11. abveq0
   12. abvne0
   13. abvgt0
   14. abvmul
   15. abvtri
   16. abv0
   17. abv1z
   18. abv1
   19. abvneg
   20. abvsubtri
   21. abvrec
   22. abvdiv
   23. abvdom
   24. abvres
   25. abvtrivd
   26. abvtriv
   27. abvpropd
4. Star rings
   1. cstf
   2. csr
   3. df-staf
   4. df-srng
   5. staffval
   6. stafval
   7. staffn
   8. issrng
   9. srngrhm
   10. srngring
   11. srngcnv
   12. srngf1o
   13. srngcl
   14. srngnvl
   15. srngadd
   16. srngmul
   17. srng1
   18. srng0
   19. issrngd
   20. idsrngd