δ_smul

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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

English

Applying δ twice yields zero: δ(n1, n2)(δ(n0, n1)(z)) = 0.

Русский

Применение δ дважды даёт ноль: δ(n1, n2)(δ(n0, n1)(z)) = 0.

LaTeX

$$$δ_{n_1,n_2}(δ_{n_0,n_1}(z)) = 0$$$

Lean4

@[simp]
theorem δ_smul (k : R) (z : Cochain F G n) : δ n m (k • z) = k • δ n m z :=
  (δ_hom R F G n m).map_smul k z

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

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

Разделы

Аффилиация

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