acyclic_of_isZero

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.acyclic_of_isZero

← MathLib Explorer

English

If K is the zero complex, then K is acyclic.

Русский

Если комплекс K нулевой, то он ацикличен.

LaTeX

$$$ \operatorname{IsZero}(K) \Rightarrow K.Acyclic $$$

Lean4

theorem acyclic_of_isZero (hK : IsZero K) : K.Acyclic :=
  by
  rw [acyclic_iff]
  intro i
  apply ShortComplex.exact_of_isZero_X₂
  exact (eval _ _ i).map_isZero hK

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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