Theorems · Theorem · group theory

MonoidHom.not_dvd_card_ker_transferSylow

∀ {G : Type u_1} [inst : Group G] {p : ℕ} (P : Sylow p G) (hP : Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P)
  [Fact (Nat.Prime p)] [Finite (Sylow p G)] [inst_3 : (↑P).FiniteIndex],
  ¬p ∣ Nat.card ↥(MonoidHom.transferSylow P hP).ker

Defined in

Mathlib.GroupTheory.Transfer

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupFactFiniteSubgroup.FiniteIndex