English
For a finite p-group G acting on α, the orbit size of any a has cardinality p^n for some n.
Русский
При действии p-группы G на множество α множество орбиты каждого элемента имеет размер p^n.
LaTeX
$$$\IsPGroup(p,G) \rightarrow {\alpha} \quad [Finite (\mathrm{orbit}\ G \alpha).Elem] \rightarrow \exists n, Nat.card(\mathrm{orbit}\ G \alpha).Elem = p^n$$$
Lean4
theorem card_orbit (a : α) [Finite (orbit G a)] : ∃ n : ℕ, Nat.card (orbit G a) = p ^ n :=
by
let ϕ := orbitEquivQuotientStabilizer G a
haveI := Finite.of_equiv (orbit G a) ϕ
haveI := (stabilizer G a).finiteIndex_of_finite_quotient
rw [Nat.card_congr ϕ]
exact hG.index (stabilizer G a)
