---

Step * 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. e = e ∈ |g|
BY
{ RWH (LemmaC `itop_unroll_hi`) 0  
THENM RW GrpNormC 0 THENA Auto }

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


By

---

Latex:
RWH  (LemmaC  `itop\_unroll\_hi`)  0   
THENM  RW  GrpNormC  0  THENA  Auto

---

Home Index