sylow_mem_fixedPoints_iff — Mathlib

English

If P is IsPGroup, then Q ∈ fixedPoints P (Sylow_p(G)) if and only if P ≤ Q.

Русский

Если P — IsPGroup, то Q ∈ фикс. точки P на Sylow_p(G) тогда и только тогда, когда P ≤ Q.

LaTeX

$$$Q \\in \\mathrm{Fix}_P(\\mathrm{Sylow}_p(G)) \\iff P \\le Q.$$$

Lean4

theorem sylow_mem_fixedPoints_iff {P : Subgroup G} (hP : IsPGroup p P) {Q : Sylow p G} :
    Q ∈ fixedPoints P (Sylow p G) ↔ P ≤ Q := by
  rw [P.sylow_mem_fixedPoints_iff, ← inf_eq_left, hP.inf_normalizer_sylow, inf_eq_left]

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