rightShift_add — Mathlib

English

The rightShift of the zero cochain is zero: right shifting zero by any amount yields zero.

Русский

Сдвиг вправо нулевого коцепного равен нулю: сдвиг вправо нулевого отображения даёт ноль.

LaTeX

$$$\\big(0:\\text{Cochain}(K,L,n)\\big).rightShift a n' hn' = 0$$$

Lean4

@[simp]
theorem rightShift_add (a n' : ℤ) (hn' : n' + a = n) :
    (γ₁ + γ₂).rightShift a n' hn' = γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn' :=
  by
  ext p q hpq
  dsimp
  simp only [rightShift_v _ a n' hn' p q hpq _ rfl, add_v, add_comp]

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