smul_eq_iff_mem_normalizer — Mathlib

English

For g ∈ G and P ∈ Sylow_p(G), the equality g · P = P holds if and only if g lies in the normalizer of P.

Русский

Для g ∈ G и P∈ Sylow_p(G) равенство g · P = P эквивалентно тому, что g лежит в нормализаторе P.

LaTeX

$$$g \\cdot P = P \\iff g \\in N_G(P).$$$

Lean4

theorem smul_eq_iff_mem_normalizer {g : G} {P : Sylow p G} : g • P = P ↔ g ∈ P.normalizer :=
  by
  rw [eq_comm, SetLike.ext_iff, ← inv_mem_iff (G := G) (H := normalizer P.toSubgroup), mem_normalizer_iff, inv_inv]
  exact
    forall_congr' fun h =>
      iff_congr Iff.rfl
        ⟨fun ⟨a, b, c⟩ => c ▸ by simpa [mul_assoc] using b, fun hh =>
          ⟨(MulAut.conj g)⁻¹ h, hh, MulAut.apply_inv_self G (MulAut.conj g) h⟩⟩

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