Description: Acommutative magma is a magma with a commutative operation. Definition 8 of BourbakiAlg1 p. 7. (Contributed by AV, 20-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | df-cmgm2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ccmgm2 | |
|
1 | vm | |
|
2 | cmgm2 | |
|
3 | cplusg | |
|
4 | 1 | cv | |
5 | 4 3 | cfv | |
6 | ccomlaw | |
|
7 | cbs | |
|
8 | 4 7 | cfv | |
9 | 5 8 6 | wbr | |
10 | 9 1 2 | crab | |
11 | 0 10 | wceq | |