goursatSnd_toAddSubgroup — Mathlib

English

If L projects surjectively onto both factors, there exists an R-linear isomorphism e: M / L.goursatFst ≃ N / L.goursatSnd such that the image of L under the quotient map equals the graph of e.

Русский

Если L проецируется сюръективно на оба множителя, существует R-линейная изоморфизм e: M / L.goursatFst ≃ N / L.goursatSnd так, что образ L под фактор-карой совпадает с графиком e.

LaTeX

$$$ \exists e : (M \! / \! L.goursatFst) \simeq_R (N \! / \! L.goursatSnd),\; \ range((L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ) \circ L.subtype) = e.graph $$$

Lean4

theorem goursatSnd_toAddSubgroup : (goursatSnd L).toAddSubgroup = L.toAddSubgroup.goursatSnd :=
  by
  ext x
  simp [mem_toAddSubgroup, goursatSnd, AddSubgroup.mem_goursatSnd]

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