rightUnshift_add — Mathlib

English

Given two cochains γ1, γ2 from K to L⟦a⟧ in degree n', the rightUnshift operation is additive in the sum: (γ1 + γ2).rightUnshift n hn = γ1.rightUnshift n hn + γ2.rightUnshift n hn, for hn: n' + a = n.

Русский

Пусть γ1, γ2 — косоценные из K в L⟦a⟧ в степени n'. Тогда правый Unshift сохраняет сложение: (γ1 + γ2).rightUnshift n hn = γ1.rightUnshift n hn + γ2.rightUnshift n hn, где hn: n' + a = n.

LaTeX

$$$(\gamma_1 + \gamma_2).rightUnshift n hn = \gamma_1.rightUnshift n hn + \gamma_2.rightUnshift n hn$$$

Lean4

@[simp]
theorem rightUnshift_add {n' a : ℤ} (γ₁ γ₂ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n) :
    (γ₁ + γ₂).rightUnshift n hn = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn :=
  by
  change (rightShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = _
  apply map_add

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