shift_zero — Mathlib

English

The rightShift operation distributes over addition: (γ1 + γ2).rightShift a n' hn' = γ1.rightShift a n' hn' + γ2.rightShift a n' hn'.

Русский

Правый сдвиг распределяется по сложению: (γ1 + γ2).rightShift a n' hn' = γ1.rightShift a n' hn' + γ2.rightShift a n' hn'.

LaTeX

$$$\\big(\\gamma_1 + \\gamma_2\\big).rightShift a n' hn' = \\gamma_1.rightShift a n' hn' + \\gamma_2.rightShift a n' hn'$$$

Lean4

@[simp]
theorem shift_zero (a : ℤ) : (0 : Cochain K L n).shift a = 0 :=
  by
  change shiftAddHom K L n a 0 = 0
  apply map_zero

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