---

Step * 1 1 2 1 of Lemma eqmod-prime-order-fixedpoints


1. n : ℕ
2. k : ℕ
3. p : ℕ
4. prime(p)
5. T : Type
6. f : T ⟶ T
7. T ~ ℕn
8. Inj(T;T;f)
9. {x:T| (f x) = x ∈ T}  ~ ℕk
10. ∀x:T. ((f^p x) = x ∈ T)
11. T ~ ℕn
12. Inj(T;T;f)
13. {x:T| (f x) = x ∈ T}  ~ ℕk
14. L : T List
15. orbit(T;f;L)
16. ||L|| | p
17. (||L|| ~ 1) ∨ (||L|| = 0 ∈ ℤ)
⊢ ||L|| = 1 ∈ ℤ
BY
{ D -1 }

1
1. n : ℕ
2. k : ℕ
3. p : ℕ
4. prime(p)
5. T : Type
6. f : T ⟶ T
7. T ~ ℕn
8. Inj(T;T;f)
9. {x:T| (f x) = x ∈ T}  ~ ℕk
10. ∀x:T. ((f^p x) = x ∈ T)
11. T ~ ℕn
12. Inj(T;T;f)
13. {x:T| (f x) = x ∈ T}  ~ ℕk
14. L : T List
15. orbit(T;f;L)
16. ||L|| | p
17. ||L|| ~ 1
⊢ ||L|| = 1 ∈ ℤ

2
1. n : ℕ
2. k : ℕ
3. p : ℕ
4. prime(p)
5. T : Type
6. f : T ⟶ T
7. T ~ ℕn
8. Inj(T;T;f)
9. {x:T| (f x) = x ∈ T}  ~ ℕk
10. ∀x:T. ((f^p x) = x ∈ T)
11. T ~ ℕn
12. Inj(T;T;f)
13. {x:T| (f x) = x ∈ T}  ~ ℕk
14. L : T List
15. orbit(T;f;L)
16. ||L|| | p
17. ||L|| = 0 ∈ ℤ
⊢ ||L|| = 1 ∈ ℤ

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}
3.  p  :  \mBbbN{}
4.  prime(p)
5.  T  :  Type
6.  f  :  T  {}\mrightarrow{}  T
7.  T  \msim{}  \mBbbN{}n
8.  Inj(T;T;f)
9.  \{x:T|  (f  x)  =  x\}    \msim{}  \mBbbN{}k
10.  \mforall{}x:T.  ((f\^{}p  x)  =  x)
11.  T  \msim{}  \mBbbN{}n
12.  Inj(T;T;f)
13.  \{x:T|  (f  x)  =  x\}    \msim{}  \mBbbN{}k
14.  L  :  T  List
15.  orbit(T;f;L)
16.  ||L||  |  p
17.  (||L||  \msim{}  1)  \mvee{}  (||L||  =  0)
\mvdash{}  ||L||  =  1


By

---

Latex:
D  -1

---

Home Index