Theorems · Theorem · group theory

IsPGroup.nonempty_fixed_point_of_prime_not_dvd_card

∀ {p : ℕ} {G : Type u_1} [inst : Group G],
  IsPGroup p G →
    ∀ [hp : Fact (Nat.Prime p)] (α : Type u_3) [inst_1 : MulAction G α],
      ¬p ∣ Nat.card α → (MulAction.fixedPoints G α).Nonempty

If a p-group acts on α and the cardinality of α is not a multiple of p then the action has a fixed point.

Defined in

Mathlib.GroupTheory.PGroup

Cited by

0 results in Mathlib

Foundations

Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupFactMulAction