---

Step * 1 of Lemma mon_nat_op_op


1. g : IAbMonoid
2. n : ℤ
3. a : |g|
4. b : |g|
⊢ (0 ⋅ (a * b)) = ((0 ⋅ a) * (0 ⋅ b)) ∈ |g|
BY
{ RWH (LemmaC `mon_nat_op_zero`) 0 
THENM RW MonNormC 0 
THEN Auto }

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  n  :  \mBbbZ{}
3.  a  :  |g|
4.  b  :  |g|
\mvdash{}  (0  \mcdot{}  (a  *  b))  =  ((0  \mcdot{}  a)  *  (0  \mcdot{}  b))


By

---

Latex:
RWH  (LemmaC  `mon\_nat\_op\_zero`)  0 
THENM  RW  MonNormC  0 
THEN  Auto

---

Home Index