δ_add

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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

English

δ is linear in the scalar: δ(n,m)(k • z) = k • δ(n,m)(z).

Русский

δ линейна по скаляру: δ(n,m)(k • z) = k • δ(n,m)(z).

LaTeX

$$$δ(n,m)(k \\cdot z) = k \\cdot δ(n,m)(z)$$$

Lean4

@[simp]
theorem δ_add (z₁ z₂ : Cochain F G n) : δ n m (z₁ + z₂) = δ n m z₁ + δ n m z₂ :=
  (δ_hom ℤ F G n m).map_add z₁ z₂

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

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

Разделы

Аффилиация

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