δ_neg

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.HomComplex.δ_neg

English

δ(n,m)(-z) = -δ(n,m)(z).

Русский

δ(n,m)(-z) = -δ(n,m)(z).

LaTeX

$$$δ(n,m)(-z) = -δ(n,m)(z)$$$

Lean4

@[simp]
theorem δ_neg (z : Cochain F G n) : δ n m (-z) = -δ n m z :=
  (δ_hom ℤ F G n m).map_neg z

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

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

Разделы

Аффилиация

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