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. srabase
   8. sraaddg
   9. sramulr
   10. srasca
   11. sravsca
   12. sraip
   13. sratset
   14. sratopn
   15. srads
   16. sraring
   17. sralmod
   18. sralmod0
   19. issubrgd
   20. rlmfn
   21. rlmval
   22. rlmval2
   23. rlmbas
   24. rlmplusg
   25. rlm0
   26. rlmsub
   27. rlmmulr
   28. rlmsca
   29. rlmsca2
   30. rlmvsca
   31. rlmtopn
   32. rlmds
   33. rlmlmod
   34. rlmlvec
   35. rlmlsm
   36. rlmvneg
   37. rlmscaf
   38. ixpsnbasval
2. Left ideals and spans
   1. clidl
   2. crsp
   3. df-lidl
   4. df-rsp
   5. lidlval
   6. rspval
   7. lidlss
   8. lidlbasel
   9. lidlssbas
   10. lidlbas
   11. islidl
   12. rnglidlmcl
   13. rngridlmcl
   14. dflidl2rng
   15. isridlrng
   16. lidl0cl
   17. lidlacl
   18. lidlnegcl
   19. lidlsubg
   20. lidlsubcl
   21. lidlmcl
   22. lidl1el
   23. lidlmcld
   24. dflidl2
   25. lidl0ALT
   26. rnglidl0
   27. lidl0
   28. lidl1ALT
   29. rnglidl1
   30. lidl1
   31. 0ringidl
   32. lidlunin0
   33. unichnlidl
   34. lidlacs
   35. rspcl
   36. rspssid
   37. rsp1
   38. rsp0
   39. rspssp
   40. rspvalint
   41. rspprop
   42. elrspsn
   43. rspsn0
   44. rspsnid
   45. pidlnz
   46. mrcrsp
   47. lidlnz
   48. drngnidl
   49. lidlrsppropd
   50. rnglidlmmgm
   51. rnglidlmsgrp
   52. rnglidlrng
   53. lidlnsg
   54. lsmidllsp
   55. lsmidl
   56. drngidl
   57. isfieldidl
   58. isfieldidl2
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. rhmpreimaidl
   30. kerlidl
   31. qusmul2idl
   32. crngridl
   33. crng2idl
   34. df2idl2crng
   35. qusmulrng
   36. quscrng
   37. qusmulcrng
   38. rhmqusnsg
   39. Condition for a non-unital ring to be unital
   40. Prime Ideals
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. Principal ideal domains
   1. cpid
   2. df-pid