d_def

Mathlib.RepresentationTheory.Homological.Resolution

URI: https://scilib.ai/kg/mathlib#Rep.barComplex.d_def

English

The barComplex differential agrees with the standard differential on the underlying carrier.

Русский

Дифференциал бар-комплекса совпадает со стандартным дифференциалом на соответствующем носителе.

LaTeX

$$$\\text{barComplex } d = d$$$

Lean4

@[simp]
theorem d_def : (barComplex k G).d (n + 1) n = d k G n :=
  ChainComplex.of_d _ _ _ _

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

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

Разделы

Аффилиация

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