double_d

Mathlib.Algebra.Homology.Double

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

Lean4

theorem double_d (h : i₀ ≠ i₁) : (double f hi₀₁).d i₀ i₁ = (doubleXIso₀ f hi₀₁).hom ≫ f ≫ (doubleXIso₁ f hi₀₁ h).inv :=
  dif_pos ⟨rfl, rfl, h⟩

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

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

Разделы

Аффилиация

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