---

Step * 1 1 of Lemma mon_nat_op_id

.....upcase..... 
1. g : IMonoid
2. n : ℤ
3. 0 < n
4. ((n - 1) ⋅ e) = e ∈ |g|
⊢ (n ⋅ e) = e ∈ |g|
BY
{ RepUnfolds ``mon_nat_op nat_op`` 0 }

1
1. g : IMonoid
2. n : ℤ
3. 0 < n
4. ((n - 1) ⋅ e) = e ∈ |g|
⊢ Π(*,e) 0 ≤ i < n. e = e ∈ |g|

---

Latex:

---

Latex:
.....upcase..... 
1.  g  :  IMonoid
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  ((n  -  1)  \mcdot{}  e)  =  e
\mvdash{}  (n  \mcdot{}  e)  =  e


By

---

Latex:
RepUnfolds  ``mon\_nat\_op  nat\_op``  0

---

Home Index