of_hasCokernel_of_hasKernel — Mathlib

English

If S has a cokernel of f and the kernel of the cokernel desc exists, then S.HasRightHomology.

Русский

Если существует кокernel для S.f и ядро(desc) кокernel существует, то у S есть правая гомология.

LaTeX

$$$ [\operatorname{HasCokernel}(S.f)] \land [\operatorname{HasKernel}(\operatorname{cokernel.desc} S.f S.g S.zero)] \Rightarrow \operatorname{HasRightHomology}(S) $$$

Lean4

instance of_hasCokernel_of_hasKernel [HasCokernel S.f] [HasKernel (cokernel.desc S.f S.g S.zero)] :
    S.HasRightHomology :=
  HasRightHomology.mk' (RightHomologyData.ofHasCokernelOfHasKernel S)

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