of_map_injective — Mathlib

English

If φ is injective and (S.map φ).Normal, then S is normal.

Русский

Если φ инъективен и (S.map φ).Normal, то S нормальна.

LaTeX

$$$ \\text{of\_map\_injective} \\; (\\mathrm{map}\\, φ\, S).Normal \\Rightarrow S.Normal $$$

Lean4

theorem of_map_injective {G H : Type*} [Group G] [Group H] {φ : G →* H} (hφ : Function.Injective φ) {L : Subgroup G}
    (n : (L.map φ).Normal) : L.Normal :=
  L.comap_map_eq_self_of_injective hφ ▸ n.comap φ

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