quotientQuotientEquivQuotientAux_mk_mk

English

Noether's third isomorphism theorem gives an isomorphism between (G/N)/(M/N) and G/M; the explicit construction is compatibly functorial with mk' maps.

Русский

Третья теорема об изоморфизма Неттера даёт изоморфизм между (G/N)/(M/N) и G/M; явная конструкция совместима с отображениями mk'.

LaTeX

$$$ (G\\!/N)\\!/ (M\\!/N) \\cong G\\!/M $$$

Lean4

@[to_additive]
theorem quotientQuotientEquivQuotientAux_mk_mk (x : G) : quotientQuotientEquivQuotientAux N M h (x : G ⧸ N) = x :=
  QuotientGroup.lift_mk' (M.map (mk' N)) _ x

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