---

Step * 1 of Lemma mon_nat_op_id


1. g : IMonoid
2. n : ℕ
⊢ (n ⋅ e) = e ∈ |g|
BY
{ NatInd 2 THEN Auto }

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

---

Latex:

---

Latex:

1.  g  :  IMonoid
2.  n  :  \mBbbN{}
\mvdash{}  (n  \mcdot{}  e)  =  e


By

---

Latex:
NatInd  2  THEN  Auto

---

Home Index