English
Compatibility between the Noether-type quotient equivalence and the mk' map: applying quotientQuotientEquivQuotientAux and then mk' equals mk' composed with the quotient equivalence.
Русский
Совместимость между эквивалентностью квотирования по Ноetherу и отображением mk': применение quotientQuotientEquivQuotientAux затем mk' равно mk' после эквивалентности квотирования.
LaTeX
$$$\\text{quotientQuotientEquivQuotientAux} \\circ \\text{mk}' = \\text{mk}' \\circ \\text{quotientQuotientEquivQuotientAux}$$$
Lean4
/-- **Noether's third isomorphism theorem** for groups: `(G / N) / (M / N) ≃* G / M`. -/
@[to_additive /-- **Noether's third isomorphism theorem** for additive groups: `(A / N) / (M / N) ≃+ A / M`. -/
]
def quotientQuotientEquivQuotient : (G ⧸ N) ⧸ M.map (QuotientGroup.mk' N) ≃* G ⧸ M :=
MonoidHom.toMulEquiv (quotientQuotientEquivQuotientAux N M h)
(QuotientGroup.map _ _ (QuotientGroup.mk' N) (Subgroup.le_comap_map _ _)) (by ext; simp) (by ext; simp)
