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


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


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{}  p
\mvdash{}  (||L||  =  1)  \mvee{}  (p  |  ||L||)


By


Latex:
(OrRight  THEN  Auto)




Home Index