normalizer_sup_eq_top' — Mathlib

English

A variant of Frattini's argument: a certain join with N equals the whole group under Frattini-like conditions.

Русский

Вариант аргумента Фратини: сумма с N даёт всю группу при условиях, аналогичных Фратини.

LaTeX

$$P.normalizer ⊔ N = ⊤$$

Lean4

/-- **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`. -/
theorem normalizer_sup_eq_top' {p : ℕ} [Fact p.Prime] {N : Subgroup G} [N.Normal] [Finite (Sylow p N)] (P : Sylow p G)
    (hP : P ≤ N) : P.normalizer ⊔ N = ⊤ := by
  rw [← normalizer_sup_eq_top (P.subtype hP), P.coe_subtype, subgroupOf_map_subtype, inf_of_le_left hP]

Похожие утверждения