---

Step * 1 1 1 1 of Lemma mon_nat_op_id


1. g : IMonoid
2. n : ℤ
3. 0 < n
4. ((n - 1) ⋅ e) = e ∈ |g|
⊢ Π(*,e) 0 ≤ i < n - 1. e = e ∈ |g|
BY
{ Fold `nat_op` 0 
THEN Fold `mon_nat_op` 0 }

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

---

Latex:

---

Latex:

1.  g  :  IMonoid
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  ((n  -  1)  \mcdot{}  e)  =  e
\mvdash{}  \mPi{}(*,e)  0  \mleq{}  i  <  n  -  1.  e  =  e


By

---

Latex:
Fold  `nat\_op`  0 
THEN  Fold  `mon\_nat\_op`  0

---

Home Index