Theorems · Theorem · group theory

MonoidHom.transferSylow_eq_pow_aux

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

Auxiliary lemma in order to state transferSylow_eq_pow.

Defined in

Mathlib.GroupTheory.Transfer

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupFactFinite