conjAct — Mathlib

English

If H is normal, then for every g ∈ G, conjugation by g leaves H invariant: g • H = H.

Русский

Если H нормальная, то при любом g ∈ G сопряжение сохраняет H: g • H = H.

LaTeX

$$$ g \cdot H = H \quad \text{for all } g \in G \text{ if } H \trianglelefteq G, $$$

Lean4

theorem conjAct {H : Subgroup G} (hH : H.Normal) (g : ConjAct G) : g • H = H :=
  have : ∀ g : ConjAct G, g • H ≤ H := fun _ => map_le_iff_le_comap.2 fun _ h => hH.conj_mem _ h _
  (this g).antisymm <| (smul_inv_smul g H).symm.trans_le (map_mono <| this _)

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