instSMul

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.HomComplex.Cocycle.instSMul

← MathLib Explorer

English

The coercion of the zero cocycle is zero in Cochain F G n.

Русский

Приведение нулевого кокцикла к элементу Cochain дает ноль.

LaTeX

$$(↑(0 : Cocycle F G n) : Cochain F G n) = 0$$

Lean4

instance : SMul R (Cocycle F G n) where
  smul r
    z :=
    ⟨r • z.1, by
      have hz := z.2
      rw [mem_iff n (n + 1) rfl] at hz ⊢
      simp only [δ_smul, hz, smul_zero]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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