isZero_zero — Mathlib

English

If the base category V has a zero object, then the zero complex in HomologicalComplex V c is a zero object in the category of chain complexes.

Русский

Если базовая категория V имеет нулевой объект, то нулевой комплекс в HomologicalComplex V c является нулевым объектом в категории цепных комплексaх.

LaTeX

$$$\\\\IsZero( zero_{HomologicalComplex V c} )$$$

Lean4

theorem isZero_zero [HasZeroObject V] : IsZero (zero : HomologicalComplex V c) :=
  by
  refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩
  all_goals
    ext
    dsimp only [zero]
    subsingleton

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