instHasZeroObject — Mathlib

English

If V has a zero object, then HomologicalComplex V c has a zero object, given by the construction zero with isZero_zero.

Русский

Если в V есть нулевой объект, то у HomologicalComplex V c тоже есть нулевой объект, задаваемый нулём вместе с свойством isZero_zero.

LaTeX

$$$\\\\HasZeroObject(HomologicalComplex\V c)$$$

Lean4

instance [HasZeroObject V] : HasZeroObject (HomologicalComplex V c) :=
  ⟨⟨zero, isZero_zero⟩⟩

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