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. 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. elrspsn
    36. mrcrsp
    37. lidlnz
    38. drngnidl
    39. lidlrsppropd
    40. rnglidlmmgm
    41. rnglidlmsgrp
    42. rnglidlrng
    43. lidlnsg
  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. qusmulrng
    35. quscrng
    36. qusmulcrng
    37. rhmqusnsg
    38. 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. Principal ideal domains
    1. cpid
    2. df-pid