Metamath Proof Explorer

Table of Contents - 21.47.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
3. 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
4. Group sum operation (extension 1)
   1. gsumsplit2f
   2. gsumdifsndf
   3. gsumfsupp