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. ringinveu
   13. isdrng4
   14. isfld
   15. flddrngd
   16. fldcrngd
   17. isdrng2
   18. drngprop
   19. drngmgp
   20. drngid
   21. drngunz
   22. drngnzr
   23. drngdomn
   24. isdrng3lem0
   25. isdrng3lem1
   26. isdrng3lem2
   27. isdrng3
   28. isdrng5
   29. drngmcl
   30. drngid2
   31. drnginvrcl
   32. drnginvrn0
   33. drnginvrcld
   34. drnginvrl
   35. drnginvrr
   36. drnginvrld
   37. drnginvrrd
   38. drngmul0or
   39. drngmulne0
   40. drngmuleq0
   41. opprdrng
   42. isdrngd
   43. isdrngrd
   44. isdrngdOLD
   45. isdrngrdOLD
   46. zrdrng
   47. drngpropd
   48. fldpropd
   49. fldidom
   50. fidomndrnglem
   51. fidomndrng
   52. fiidomfld
   53. rng1nnzr
   54. ring1zr
   55. ringen1zr0
   56. rng1nfld
   57. issubdrg
   58. drhmsubc
   59. drngcat
   60. fldcat
   61. fldc
   62. 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