Metamath Proof Explorer

Table of Contents - 21.20.7. Monoids

See ccmn and subsequents. The first few statements of this subsection can be put very early after ccmn. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups.

Relabel cabl to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency.

1. bj-smgrpssmgm
2. bj-smgrpssmgmel
3. bj-mndsssmgrp
4. bj-mndsssmgrpel
5. bj-cmnssmnd
6. bj-cmnssmndel
7. bj-grpssmnd
8. bj-grpssmndel
9. bj-ablssgrp
10. bj-ablssgrpel
11. bj-ablsscmn
12. bj-ablsscmnel
13. bj-modssabl
14. bj-vecssmod
15. bj-vecssmodel
16. Finite sums in monoids
    1. cfinsum
    2. df-bj-finsum
    3. bj-finsumval0