sylow_mem_fixedPoints_iff — Mathlib

English

For any subgroup H ≤ G and P ∈ Sylow_p(G), P belongs to the fixed points of H acting on Sylow_p(G) if and only if H ≤ N_G(P).

Русский

Для любого H ≤ G и P ∈ Sylow_p(G), P фиксируется действием H на Sylow_p(G) тогда и только тогда, когда H ≤ N_G(P).

LaTeX

$$$P \\in \\mathrm{Fix}_H(\\mathrm{Sylow}_p(G)) \\iff H \\le N_G(P).$$$

Lean4

theorem sylow_mem_fixedPoints_iff (H : Subgroup G) {P : Sylow p G} : P ∈ fixedPoints H (Sylow p G) ↔ H ≤ P.normalizer :=
  by simp_rw [SetLike.le_def, ← Sylow.smul_eq_iff_mem_normalizer]; exact Subtype.forall

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