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. drngringd
   10. drnggrpd
   11. drnggrp
   12. isfld
   13. flddrngd
   14. fldcrngd
   15. isdrng2
   16. drngprop
   17. drngmgp
   18. drngid
   19. drngunz
   20. drngnzr
   21. drngdomn
   22. drngmcl
   23. drngmclOLD
   24. drngid2
   25. drnginvrcl
   26. drnginvrn0
   27. drnginvrcld
   28. drnginvrl
   29. drnginvrr
   30. drnginvrld
   31. drnginvrrd
   32. drngmul0or
   33. drngmul0orOLD
   34. drngmulne0
   35. drngmuleq0
   36. opprdrng
   37. isdrngd
   38. isdrngrd
   39. isdrngdOLD
   40. isdrngrdOLD
   41. drngpropd
   42. fldpropd
   43. fldidom
   44. fidomndrnglem
   45. fidomndrng
   46. fiidomfld
   47. rng1nnzr
   48. ring1zr
   49. rngen1zr
   50. ringen1zr
   51. rng1nfld
   52. issubdrg
   53. drhmsubc
   54. drngcat
   55. fldcat
   56. fldc
   57. fldhmsubc
2. Sub-division rings
   1. csdrg
   2. df-sdrg
   3. issdrg
   4. sdrgrcl
   5. sdrgdrng
   6. sdrgsubrg
   7. sdrgid
   8. sdrgss
   9. sdrgbas
   10. issdrg2
   11. sdrgunit
   12. imadrhmcl
   13. fldsdrgfld
   14. acsfn1p
   15. subrgacs
   16. sdrgacs
   17. cntzsdrg
   18. subdrgint
   19. sdrgint
   20. primefld
   21. primefld0cl
   22. primefld1cl
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. abvtrivg
   27. abvtriv
   28. abvpropd
   29. abvn0b
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
5. Totally ordered rings and fields
   1. corng
   2. cofld
   3. df-orng
   4. df-ofld
   5. isorng
   6. orngring
   7. orngogrp
   8. isofld
   9. orngmul
   10. orngsqr
   11. ornglmulle
   12. orngrmulle
   13. ornglmullt
   14. orngrmullt
   15. orngmullt
   16. ofldfld
   17. ofldtos
   18. orng0le1
   19. ofldlt1
   20. suborng
   21. subofld