English
Similarly, the second Goursat component of L, seen as a submodule of N, coincides with the corresponding projection.
Русский
Аналогично, вторая компонента Гурсата L, рассматриваемая как подмодуль в N, совпадает с соответствующей проекцией.
LaTeX
$$$ (goursatSnd\; L).toAddSubgroup = L.toAddSubgroup.goursatSnd $$$
Lean4
/-- For `L` a subgroup of `M × N`, `L.goursatSnd` is the kernel of the projection map `L → M`,
considered as a subgroup of `N`.
This is the second subgroup appearing in Goursat's lemma. See `Subgroup.goursat`. -/
def goursatSnd : Submodule R N :=
(LinearMap.ker <| (LinearMap.fst R M N).comp L.subtype).map ((LinearMap.snd R M N).comp L.subtype)
