Theorems · Theorem · group theory

Sylow.conj_eq_normalizer_conj_of_mem_centralizer

∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (x g : G),
  x ∈ Subgroup.centralizer ↑P →
    g⁻¹ * x * g ∈ Subgroup.centralizer ↑P → ∃ n ∈ Subgroup.normalizer ↑P, g⁻¹ * x * g = n⁻¹ * x * n

Defined in

Mathlib.GroupTheory.Sylow

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupFactFinite