map — Mathlib

English

If H is normal in G and f: G → N is surjective, then f(H) is normal in N.

Русский

Пусть H ⊲ G. Если f: G → N сюръективно, то образ H в N является нормальной подгруппой.

LaTeX

$$$ f(H) \\\\trianglelefteq N $$$

Lean4

@[to_additive]
theorem map {H : Subgroup G} (h : H.Normal) (f : G →* N) (hf : Function.Surjective f) : (H.map f).Normal :=
  by
  rw [← normalizer_eq_top_iff, ← top_le_iff, ← f.range_eq_top_of_surjective hf, f.range_eq_map, ← H.normalizer_eq_top]
  exact le_normalizer_map _

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