succ_exact — Mathlib

English

The short complex formed by the module maps is exact.

Русский

Короткий комплекс, образованный отображениями модулей, является точным.

LaTeX

$$$\\text{succ\\_exact}: \\text{ShortComplex.mk}(\\text{ModuleCat.ofHom}(\\pi_s C o)) \\text{(ModuleCat.ofHom}(\\mathrm{Linear\\_CC'} C hsC ho)) \\dots$.Exact$$

Lean4

theorem succ_exact :
    (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho))
        (by ext : 2; apply CC_comp_zero)).Exact :=
  by
  rw [ShortComplex.moduleCat_exact_iff]
  intro f
  exact CC_exact C hC hsC ho

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