English
For a finite p-group G acting on α, the orbit size is p^n for some n.
Русский
Для конечной p-группы G, действующей на α, размер орбиты элемента равен p^n для некоторого n.
LaTeX
$$$\IsPGroup(p,G) \rightarrow {\alpha} [MulAction G \alpha] [Finite(\mathrm{orbit}\ G \alpha).Elem], \exists n, Nat.card(\mathrm{orbit}\ G \alpha).Elem = p^n$$$
Lean4
/-- If a p-group acts on `α` and the cardinality of `α` is a multiple
of `p`, and the action has one fixed point, then it has another fixed point. -/
theorem exists_fixed_point_of_prime_dvd_card_of_fixed_point (hpα : p ∣ Nat.card α) {a : α} (ha : a ∈ fixedPoints G α) :
∃ b, b ∈ fixedPoints G α ∧ a ≠ b :=
by
have hpf : p ∣ Nat.card (fixedPoints G α) :=
Nat.modEq_zero_iff_dvd.mp ((hG.card_modEq_card_fixedPoints α).symm.trans hpα.modEq_zero_nat)
have hα : 1 < Nat.card (fixedPoints G α) :=
(Fact.out (p := p.Prime)).one_lt.trans_le (Nat.le_of_dvd (Finite.card_pos_iff.2 ⟨⟨a, ha⟩⟩) hpf)
rw [Finite.one_lt_card_iff_nontrivial] at hα
exact
let ⟨⟨b, hb⟩, hba⟩ := exists_ne (⟨a, ha⟩ : fixedPoints G α)
⟨b, hb, fun hab => hba (by simp_rw [hab])⟩
