Theorems · Theorem · group theory

IsPGroup.commutator_eq_bot_or_commutator_eq_self

∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] {P K : Subgroup G} [IsCyclic ↥P],
  IsPGroup p ↥P → K ≤ Subgroup.normalizer ↑P → (Nat.card ↥P).Coprime (Nat.card ↥K) → ⁅K, P⁆ = ⊥ ∨ ⁅K, P⁆ = P

If a cyclic p-subgroup P acts by conjugation on a subgroup K of coprime order, then either ⁅K, P⁆ = ⊥ or ⁅K, P⁆ = P.

Defined in

Mathlib.GroupTheory.SpecificGroups.ZGroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupFactIsCyclic