English
Let p be a prime and α a finite set with p not dividing |α|. If σ^{p^n} = id for a permutation σ of α, then there exists a fixed point a with σ(a) = a.
Русский
Пусть p — простое, и |α| не делится на p. Если σ^{p^n} = id для перестановки σ над α, то существует a ∈ α такое, что σ(a) = a.
LaTeX
$$$(p \\text{ prime}) \\land (p \nmid |\\alpha|) \\land (\\sigma^{p^n} = 1) \\implies \\exists a \\in \\alpha:\\ \\sigma(a) = a$$$
Lean4
theorem exists_fixed_point_of_prime {p n : ℕ} [hp : Fact p.Prime] (hα : ¬p ∣ Fintype.card α) {σ : Perm α}
(hσ : σ ^ p ^ n = 1) : ∃ a : α, σ a = a := by
classical
contrapose! hα
simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα
exact
Nat.modEq_zero_iff_dvd.1
((congr_arg _ (Finset.card_eq_zero.2 (compl_eq_bot.2 hα))).mp (card_compl_support_modEq hσ).symm)
