zero

Mathlib.Algebra.Homology.HomologicalComplex

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

Lean4

/-- The zero complex -/
noncomputable def zero [HasZeroObject V] : HomologicalComplex V c
    where
  X _ := 0
  d _ _ := 0

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

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

Разделы

Аффилиация

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