exact_subtype_ker_map — Mathlib

English

For any linear map g: N → P, the inclusion of ker(g) into N followed by g is exact; i.e. Im(Submodule.subtype(ker g)) = ker(g).

Русский

Для линейного отображения g: N → P вложение ker(g) в N и затем применение g образуют точность; Im(ker g ⊆ N) = ker(g).

LaTeX

$$$$ \\operatorname{Im}(\\operatorname{Submodule.subtype}(\\ker g)) = \\ker g. $$$$

Lean4

theorem exact_subtype_ker_map (g : N →ₗ[R] P) : Exact (Submodule.subtype (ker g)) g :=
  exact_iff.mpr <| (Submodule.range_subtype _).symm

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