normal_goursatSnd — Mathlib

English

Goursat's lemma describes subgroups of a product: I is determined by appropriate subgroups of G and H and a normal isomorphism between quotients.

Русский

Лемма Гурсо описывает подгруппы произведения: I задаётся подходящими подгруппами G и H и нормальным изоморфизмом между частными группами.

LaTeX

$$$$\\exists (G' \\le G)\n\\exists (H' \\le H)\n\\exists (M \\lhd G') (N \\lhd H') (e: G'/M \\cong H'/N),\\; I = (\\text{graph}(e)^{\\,*}).$$$

Lean4

@[to_additive]
theorem normal_goursatSnd : I.goursatSnd.Normal :=
  .map inferInstance _ hI₂

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