---

Step * of Lemma rotate-by-cyclic-map

∀[n,i:ℕ].  rotate-by(n;i) ∈ cyclic-map(ℕn) supposing gcd(i;n) = 1 ∈ ℤ
BY
{ (Auto THEN MemTypeCD) }

1
1. n : ℕ
2. i : ℕ
3. gcd(i;n) = 1 ∈ ℤ
⊢ rotate-by(n;i) ∈ ℕn →⟶ ℕn

2
.....set predicate..... 
1. n : ℕ
2. i : ℕ
3. gcd(i;n) = 1 ∈ ℤ
⊢ ∀x,y:ℕn.  ∃n@0:ℕ. ((rotate-by(n;i)^n@0 x) = y ∈ ℕn)

3
.....wf..... 
1. n : ℕ
2. i : ℕ
3. gcd(i;n) = 1 ∈ ℤ
4. f : ℕn →⟶ ℕn
⊢ ∀x,y:ℕn.  ∃n@0:ℕ. ((f^n@0 x) = y ∈ ℕn) ∈ Type

---

Latex:

---

Latex:
\mforall{}[n,i:\mBbbN{}].    rotate-by(n;i)  \mmember{}  cyclic-map(\mBbbN{}n)  supposing  gcd(i;n)  =  1


By

---

Latex:
(Auto  THEN  MemTypeCD)

---

Home Index