d_sub_one_zero

Mathlib.Algebra.Homology.Embedding.Connect

URI: https://scilib.ai/kg/mathlib#CochainComplex.ConnectData.d_sub_one_zero

English

The value d(-1,0) equals the distinguished d0 edge in the data.

Русский

Значение d(-1,0) равно выбранному edge d0 в данных.

LaTeX

$$d_sub_one_zero : h.d(-1) 0 = h.d₀$$

Lean4

@[simp]
theorem d_sub_one_zero : h.d (-1) 0 = h.d₀ :=
  rfl

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

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

Разделы

Аффилиация

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