Metamath Proof Explorer

Table of Contents - 10.7. Ideals

1. The subring algebra; ideals
   1. csra
   2. crglmod
   3. clidl
   4. crsp
   5. df-sra
   6. df-rgmod
   7. df-lidl
   8. df-rsp
   9. sraval
   10. sralem
   11. srabase
   12. sraaddg
   13. sramulr
   14. srasca
   15. sravsca
   16. sraip
   17. sratset
   18. sratopn
   19. srads
   20. sralmod
   21. sralmod0
   22. issubrngd2
   23. rlmfn
   24. rlmval
   25. lidlval
   26. rspval
   27. rlmval2
   28. rlmbas
   29. rlmplusg
   30. rlm0
   31. rlmsub
   32. rlmmulr
   33. rlmsca
   34. rlmsca2
   35. rlmvsca
   36. rlmtopn
   37. rlmds
   38. rlmlmod
   39. rlmlvec
   40. rlmlsm
   41. rlmvneg
   42. rlmscaf
   43. ixpsnbasval
   44. lidlss
   45. islidl
   46. lidl0cl
   47. lidlacl
   48. lidlnegcl
   49. lidlsubg
   50. lidlsubcl
   51. lidlmcl
   52. lidl1el
   53. lidl0
   54. lidl1
   55. lidlacs
   56. rspcl
   57. rspssid
   58. rsp1
   59. rsp0
   60. rspssp
   61. mrcrsp
   62. lidlnz
   63. drngnidl
   64. lidlrsppropd
2. Two-sided ideals and quotient rings
   1. c2idl
   2. df-2idl
   3. 2idlval
   4. 2idlcpbl
   5. qus1
   6. qusring
   7. qusrhm
   8. crngridl
   9. crng2idl
   10. quscrng
3. Principal ideal rings. Divisibility in the integers
   1. clpidl
   2. clpir
   3. df-lpidl
   4. df-lpir
   5. lpival
   6. islpidl
   7. lpi0
   8. lpi1
   9. islpir
   10. lpiss
   11. islpir2
   12. lpirring
   13. drnglpir
   14. rspsn
   15. lidldvgen
   16. lpigen
4. Nonzero rings and zero rings
   1. cnzr
   2. df-nzr
   3. isnzr
   4. nzrnz
   5. nzrring
   6. drngnzr
   7. isnzr2
   8. isnzr2hash
   9. opprnzr
   10. ringelnzr
   11. nzrunit
   12. subrgnzr
   13. 0ringnnzr
   14. 0ring
   15. 0ring01eq
   16. 01eq0ring
   17. 0ring01eqbi
   18. rng1nnzr
   19. ring1zr
   20. rngen1zr
   21. ringen1zr
   22. rng1nfld
5. Left regular elements. More kinds of rings
   1. crlreg
   2. cdomn
   3. cidom
   4. cpid
   5. df-rlreg
   6. df-domn
   7. df-idom
   8. df-pid
   9. rrgval
   10. isrrg
   11. rrgeq0i
   12. rrgeq0
   13. rrgsupp
   14. rrgss
   15. unitrrg
   16. isdomn
   17. domnnzr
   18. domnring
   19. domneq0
   20. domnmuln0
   21. isdomn2
   22. domnrrg
   23. opprdomn
   24. abvn0b
   25. drngdomn
   26. isidom
   27. fldidom
   28. fidomndrnglem
   29. fidomndrng
   30. fiidomfld