---

Step * of Lemma mon_itop_perm_invar

∀g:IAbMonoid. ∀n:ℕ. ∀E:ℕn ⟶ |g|. ∀p:Sym(n).  ((Π 0 ≤ j < n. E[p.f j]) = (Π 0 ≤ j < n. E[j]) ∈ |g|)
BY
{ (RepeatMFor 3 (D 0) THENA Auto) }

1
1. g : IAbMonoid
2. n : ℕ
3. E : ℕn ⟶ |g|
⊢ ∀p:Sym(n). ((Π 0 ≤ j < n. E[p.f j]) = (Π 0 ≤ j < n. E[j]) ∈ |g|)

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  \mforall{}n:\mBbbN{}.  \mforall{}E:\mBbbN{}n  {}\mrightarrow{}  |g|.  \mforall{}p:Sym(n).    ((\mPi{}  0  \mleq{}  j  <  n.  E[p.f  j])  =  (\mPi{}  0  \mleq{}  j  <  n.  E[j]))


By

---

Latex:
(RepeatMFor  3  (D  0)  THENA  Auto)

---

Home Index