---

Step * of Lemma mon_nat_op_op

∀[g:IAbMonoid]. ∀[n:ℕ]. ∀[a,b:|g|].  ((n ⋅ (a * b)) = ((n ⋅ a) * (n ⋅ b)) ∈ |g|)
BY
{ D 0 THENM D 0 THENM NatInd (-1) 
THEN Auto }

1
1. g : IAbMonoid
2. n : ℤ
3. a : |g|
4. b : |g|
⊢ (0 ⋅ (a * b)) = ((0 ⋅ a) * (0 ⋅ b)) ∈ |g|

2
1. g : IAbMonoid
2. n : ℤ
3. 0 < n
4. ∀[a,b:|g|].  (((n - 1) ⋅ (a * b)) = (((n - 1) ⋅ a) * ((n - 1) ⋅ b)) ∈ |g|)
5. a : |g|
6. b : |g|
⊢ (n ⋅ (a * b)) = ((n ⋅ a) * (n ⋅ b)) ∈ |g|

---

Latex:

---

Latex:
\mforall{}[g:IAbMonoid].  \mforall{}[n:\mBbbN{}].  \mforall{}[a,b:|g|].    ((n  \mcdot{}  (a  *  b))  =  ((n  \mcdot{}  a)  *  (n  \mcdot{}  b)))


By

---

Latex:
D  0  THENM  D  0  THENM  NatInd  (-1) 
THEN  Auto

---

Home Index