---

Step * of Lemma int_mul_mon_wf

<ℤ,*> ∈ AbMon
BY
{ ((Unfold `int_mul_mon` 0 THENM BLemma `mk_abmonoid`) THENA Auto) }

1
Assoc(ℤ;λx,y. (x * y))

2
Ident(ℤ;λx,y. (x * y);1)

3
Comm(ℤ;λx,y. (x * y))

---

Latex:

---

Latex:
<\mBbbZ{},*>  \mmember{}  AbMon


By

---

Latex:
((Unfold  `int\_mul\_mon`  0  THENM  BLemma  `mk\_abmonoid`)  THENA  Auto)

---

Home Index