ab_exact_iff_ker_le_range — Mathlib

English

Let S be a ShortComplex in Ab. Then S is exact if and only if the kernel of g is contained in the image of f; equivalently, ker(g) ≤ im(f).

Русский

Пусть S — краткая точная последовательность в абелевых группах. Тогда точность S эквивалентна тому, что ядро g содержится в образе f; то есть ker(g) ⊆ im(f).

LaTeX

$$$$ S.Exact \\iff \\ker(g) \\le \\mathrm{im}(f). $$$$

Lean4

theorem ab_exact_iff_ker_le_range : S.Exact ↔ S.g.hom.ker ≤ S.f.hom.range :=
  S.ab_exact_iff

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