Theorems · Theorem · group theory

Sylow.normalizer_sup_eq_top

∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] {N : Subgroup G} [N.Normal] [Finite (Sylow p ↥N)]
  (P : Sylow p ↥N), Subgroup.normalizer ↑(Subgroup.map N.subtype ↑P) ⊔ N = ⊤

Frattini's Argument: If N is a normal subgroup of G, and if P is a Sylow p-subgroup of N, then N_G(P) ⊔ N = G.

Defined in

Mathlib.GroupTheory.Sylow

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupFactSubgroup.NormalFinite