Metamath Proof Explorer


Table of Contents - 20.43.16. Monoids (extension)

  1. Auxiliary theorems
    1. ovn0dmfun
    2. xpsnopab
    3. xpiun
    4. ovn0ssdmfun
    5. fnxpdmdm
    6. cnfldsrngbas
    7. cnfldsrngadd
    8. cnfldsrngmul
  2. Magmas, Semigroups and Monoids (extension)
    1. plusfreseq
    2. mgmplusfreseq
    3. 0mgm
    4. mgmpropd
    5. ismgmd
  3. Magma homomorphisms and submagmas
    1. cmgmhm
    2. csubmgm
    3. df-mgmhm
    4. df-submgm
    5. mgmhmrcl
    6. submgmrcl
    7. ismgmhm
    8. mgmhmf
    9. mgmhmpropd
    10. mgmhmlin
    11. mgmhmf1o
    12. idmgmhm
    13. issubmgm
    14. issubmgm2
    15. rabsubmgmd
    16. submgmss
    17. submgmid
    18. submgmcl
    19. submgmmgm
    20. submgmbas
    21. subsubmgm
    22. resmgmhm
    23. resmgmhm2
    24. resmgmhm2b
    25. mgmhmco
    26. mgmhmima
    27. mgmhmeql
    28. submgmacs
    29. ismhm0
    30. mhmismgmhm
  4. Examples and counterexamples for magmas, semigroups and monoids (extension)
    1. opmpoismgm
    2. copissgrp
    3. copisnmnd
    4. 0nodd
    5. 1odd
    6. 2nodd
    7. oddibas
    8. oddiadd
    9. oddinmgm
    10. nnsgrpmgm
    11. nnsgrp
    12. nnsgrpnmnd
    13. nn0mnd
  5. Group sum operation (extension 1)
    1. gsumsplit2f
    2. gsumdifsndf
    3. gsumfsupp