English
If p divides the size of the finite set α and σ^ (p^n) = id with σ a permutation of α, and a is fixed by σ, then there exists a fixed point b different from a.
Русский
Если p делит размер конечного множества α и σ^ (p^n) = id для перестановки σ над α, причём существует фиксированная точка a, то существует другая фиксированная точка b, отличная от a.
LaTeX
$$$(p \\mid |\\alpha|) \\land (\\sigma^{p^n} = 1) \\land (\\sigma(a) = a) \\implies \\exists b:\\, \\sigma(b) = b \\land b \\neq a$$$
Lean4
theorem exists_fixed_point_of_prime' {p n : ℕ} [hp : Fact p.Prime] (hα : p ∣ Fintype.card α) {σ : Perm α}
(hσ : σ ^ p ^ n = 1) {a : α} (ha : σ a = a) : ∃ b : α, σ b = b ∧ b ≠ a := by
classical
have h : ∀ b : α, b ∈ σ.supportᶜ ↔ σ b = b := fun b => by rw [Finset.mem_compl, mem_support, Classical.not_not]
obtain ⟨b, hb1, hb2⟩ :=
Finset.exists_mem_ne
(hp.out.one_lt.trans_le
(Nat.le_of_dvd (Finset.card_pos.mpr ⟨a, (h a).mpr ha⟩)
(Nat.modEq_zero_iff_dvd.mp ((card_compl_support_modEq hσ).trans (Nat.modEq_zero_iff_dvd.mpr hα)))))
a
exact ⟨b, (h b).mp hb1, hb2⟩
