English
As above, in the same setting, another formulation of the fixed points congruence holds.
Русский
Как и выше, в той же постановке — другая формулировка конгруэнтности фиксированных точек.
LaTeX
$$$\IsPGroup(p,G) \rightarrow [hp : Fact (Nat.Prime p)] (\alpha) [MulAction G \alpha] [Finite \alpha], p.ModEq (Nat.card \alpha) (Nat.card (fixedPoints G \alpha).Elem)$$$
Lean4
/-- If a p-group acts on `α` and the cardinality of `α` is not a multiple
of `p` then the action has a fixed point. -/
theorem nonempty_fixed_point_of_prime_not_dvd_card (α) [MulAction G α] (hpα : ¬p ∣ Nat.card α) :
(fixedPoints G α).Nonempty :=
have : Finite α := Nat.finite_of_card_ne_zero (fun h ↦ (h ▸ hpα) (dvd_zero p))
@Set.Nonempty.of_subtype _ _
(by
rw [← Finite.card_pos_iff, pos_iff_ne_zero]
contrapose! hpα
rw [← Nat.modEq_zero_iff_dvd, ← hpα]
exact hG.card_modEq_card_fixedPoints α)
