Step
*
1
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
⊢ (||L|| = 1 ∈ ℤ) ∨ (p | ||L||)
BY
{ ((FLemma `divides-prime` [-1] THENA Auto) THEN 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|| ~ p
⊢ (||L|| = 1 ∈ ℤ) ∨ (p | ||L||)
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|| ~ 1) ∨ (||L|| = 0 ∈ ℤ)
⊢ (||L|| = 1 ∈ ℤ) ∨ (p | ||L||)
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
\mvdash{} (||L|| = 1) \mvee{} (p | ||L||)
By
Latex:
((FLemma `divides-prime` [-1] THENA Auto) THEN D -1)
Home
Index