Theorems · Theorem · group theory

IsPGroup.exists_fixed_point_of_prime_dvd_card_of_fixed_point

∀ {p : ℕ} {G : Type u_1} [inst : Group G],
  IsPGroup p G →
    ∀ [hp : Fact (Nat.Prime p)] (α : Type u_2) [inst_1 : MulAction G α] [Finite α],
      p ∣ Nat.card α → ∀ {a : α}, a ∈ MulAction.fixedPoints G α → ∃ b ∈ MulAction.fixedPoints G α, a ≠ b

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.

Defined in

Mathlib.GroupTheory.PGroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupFactMulActionFinite