inf_normalizer_sylow — Mathlib

English

For an IsPGroup p-P inside P and Q Sylow p G, P ∩ Q.normalizer = P ∩ Q.

Русский

Для P, являющегося IsPGroup, и Q Sylow p G выполняется P ∩ N_G(Q) = P ∩ Q.

LaTeX

$$$P \\cap Q^{\\mathrm{normalizer}} = P \\cap Q,$$$

Lean4

theorem inf_normalizer_sylow {P : Subgroup G} (hP : IsPGroup p P) (Q : Sylow p G) : P ⊓ Q.normalizer = P ⊓ Q :=
  le_antisymm
    (le_inf inf_le_left (sup_eq_right.mp (Q.3 (hP.to_inf_left.to_sup_of_normal_right' Q.2 inf_le_right) le_sup_right)))
    (inf_le_inf_left P le_normalizer)

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