single₀ObjXSelf — Mathlib

English

There is a canonical identity-like isomorphism between the object X and the degree-zero component of the corresponding single₀ complex.

Русский

Существует каноническое подобие в виде идентичности между объектом X и нулевой степенью соответствующего single₀ комплекса.

LaTeX

$$$\\mathrm{single}_0\\mathrm{ObjXSelf}(X) = \\mathrm{Iso.identity}$$$

Lean4

@[simp]
theorem single₀ObjXSelf (X : V) : HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 X = Iso.refl _ :=
  rfl

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