d

Mathlib.Algebra.Homology.Embedding.Extend

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

Lean4

/-- Auxiliary definition for the `d` field of `HomologicalComplex.extend`. -/
noncomputable def d : ∀ (i j : Option ι), extend.X K i ⟶ extend.X K j
  | none, _ => 0
  | some i, some j => K.d i j
  | some _, none => 0

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

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

Разделы

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

Аффилиация

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