English
For a normal N and a second subgroup H of G, there is an isomorphism H/(H∩N) ≅ (HN)/N; for two subgroups with N normal, the isomorphism extends to H and N within G.
Русский
Для нормальной N и второй подгруппы H внутри G существует изоморфизм H/(H∩N) ≅ (HN)/N; при двух подгруппах с нормализацией N изоморфизм распространяется на H и N внутри G.
LaTeX
$$$H /(H\\cap N) \\cong (H\\!\\cup\\! N)/N$$$
Lean4
/-- **Noether's second isomorphism theorem**: given two subgroups `H` and `N` of a group `G`,
where `N` is normal, defines an isomorphism between `H/(H ∩ N)` and `(HN)/N`. -/
@[to_additive /-- Noether's second isomorphism theorem: given two subgroups `H` and `N` of a group
`G`, where `N` is normal, defines an isomorphism between `H/(H ∩ N)` and `(H + N)/N`. -/
]
noncomputable def quotientInfEquivProdNormalQuotient (H N : Subgroup G) [hN : N.Normal] :
H ⧸ N.subgroupOf H ≃* (H ⊔ N : Subgroup G) ⧸ N.subgroupOf (H ⊔ N) :=
quotientInfEquivProdNormalizerQuotient H N le_normalizer_of_normal
