Theorems · Theorem · group theory

Sylow.conj_eq_normalizer_conj_of_mem

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

Defined in

Mathlib.GroupTheory.Sylow

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupFactFiniteIsMulCommutative