---

Step * 1 1 of Lemma mon_itop_perm_invar


1. g : IAbMonoid
2. n : ℕ
3. E : ℕn ⟶ |g|
⊢ (Π 0 ≤ j < n. E (id_perm().f j)) = (Π 0 ≤ j < n. E j) ∈ |g|
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  n  :  \mBbbN{}
3.  E  :  \mBbbN{}n  {}\mrightarrow{}  |g|
\mvdash{}  (\mPi{}  0  \mleq{}  j  <  n.  E  (id\_perm().f  j))  =  (\mPi{}  0  \mleq{}  j  <  n.  E  j)


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index