isZero_X

Mathlib.Algebra.Homology.Embedding.Extend

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.extend.isZero_X

English

The X component in the extended complex is zero in the left/right extremes when the index is none.

Русский

Компонента X в расширенном комплексе нулевая на крайних позициях, когда индекс none.

LaTeX

$$isZero_X {i : Option ι} (hi : i = none) : IsZero (X K i)$$

Lean4

theorem isZero_X {i : Option ι} (hi : i = none) : IsZero (X K i) :=
  by
  subst hi
  exact Limits.isZero_zero _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru