Metamath Proof Explorer

Table of Contents - 10.7. Subring algebras and ideals

1. Subring algebras
   1. csra
   2. crglmod
   3. df-sra
   4. df-rgmod
   5. sraval
   6. sralem
   7. sralemOLD
   8. srabase
   9. srabaseOLD
   10. sraaddg
   11. sraaddgOLD
   12. sramulr
   13. sramulrOLD
   14. srasca
   15. srascaOLD
   16. sravsca
   17. sravscaOLD
   18. sraip
   19. sratset
   20. sratsetOLD
   21. sratopn
   22. srads
   23. sradsOLD
   24. sraring
   25. sralmod
   26. sralmod0
   27. issubrgd
   28. rlmfn
   29. rlmval
   30. rlmval2
   31. rlmbas
   32. rlmplusg
   33. rlm0
   34. rlmsub
   35. rlmmulr
   36. rlmsca
   37. rlmsca2
   38. rlmvsca
   39. rlmtopn
   40. rlmds
   41. rlmlmod
   42. rlmlvec
   43. rlmlsm
   44. rlmvneg
   45. rlmscaf
   46. ixpsnbasval
2. Left ideals and spans
   1. clidl
   2. crsp
   3. df-lidl
   4. df-rsp
   5. lidlval
   6. rspval
   7. lidlss
   8. lidlssbas
   9. lidlbas
   10. islidl
   11. rnglidlmcl
   12. rngridlmcl
   13. dflidl2rng
   14. isridlrng
   15. lidl0cl
   16. lidlacl
   17. lidlnegcl
   18. lidlsubg
   19. lidlsubcl
   20. lidlmcl
   21. lidl1el
   22. dflidl2
   23. lidl0ALT
   24. rnglidl0
   25. lidl0
   26. lidl1ALT
   27. rnglidl1
   28. lidl1
   29. lidlacs
   30. rspcl
   31. rspssid
   32. rsp1
   33. rsp0
   34. rspssp
   35. mrcrsp
   36. lidlnz
   37. drngnidl
   38. lidlrsppropd
   39. rnglidlmmgm
   40. rnglidlmsgrp
   41. rnglidlrng
3. Two-sided ideals and quotient rings
   1. c2idl
   2. df-2idl
   3. 2idlval
   4. isridl
   5. 2idlelb
   6. 2idllidld
   7. 2idlridld
   8. df2idl2rng
   9. df2idl2
   10. ridl0
   11. ridl1
   12. 2idl0
   13. 2idl1
   14. 2idlss
   15. 2idlbas
   16. 2idlelbas
   17. rng2idlsubrng
   18. rng2idlnsg
   19. rng2idl0
   20. rng2idlsubgsubrng
   21. rng2idlsubgnsg
   22. rng2idlsubg0
   23. 2idlcpblrng
   24. 2idlcpbl
   25. qus2idrng
   26. qus1
   27. qusring
   28. qusrhm
   29. qusmul2
   30. crngridl
   31. crng2idl
   32. qusmulrng
   33. quscrng
   34. Condition for a non-unital ring to be unital
4. 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
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. isdomn3
   24. isdomn5
   25. isdomn4
   26. opprdomn
   27. abvn0b
   28. drngdomn
   29. isidom
   30. idomdomd
   31. idomcringd
   32. idomringd
   33. fldidom
   34. fldidomOLD
   35. fidomndrnglem
   36. fidomndrng
   37. fiidomfld