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. srascaOLD
    12. sravsca
    13. sravscaOLD
    14. sraip
    15. sratset
    16. sratopn
    17. srads
    18. sraring
    19. sralmod
    20. sralmod0
    21. issubrgd
    22. rlmfn
    23. rlmval
    24. rlmval2
    25. rlmbas
    26. rlmplusg
    27. rlm0
    28. rlmsub
    29. rlmmulr
    30. rlmsca
    31. rlmsca2
    32. rlmvsca
    33. rlmtopn
    34. rlmds
    35. rlmlmod
    36. rlmlvec
    37. rlmlsm
    38. rlmvneg
    39. rlmscaf
    40. 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