leftShift_neg — Mathlib

English

The leftUnshift of the zero cochain is zero: zero maps to zero under leftUnshift.

Русский

Левая операция leftUnshift нулевого коцепного отображения даёт ноль.

LaTeX

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

Lean4

@[simp]
theorem leftShift_neg (a n' : ℤ) (hn' : n + a = n') : (-γ).leftShift a n' hn' = -γ.leftShift a n' hn' :=
  by
  change leftShiftAddEquiv K L n a n' hn' (-γ) = _
  apply map_neg

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