leftShift_zero — Mathlib

English

Symmetric statement: the leftShiftAddEquiv respects the symmetry between K and L in the sense of the additive equivalence for shifting.

Русский

Симметричное утверждение: leftShiftAddEquiv сохраняет симметрию между K и L в контексте аддитивной эквивалентности для сдвига.

LaTeX

$$$\\text{LeftShiftAddEquiv}_{sym}$$$

Lean4

@[simp]
theorem leftShift_zero (a n' : ℤ) (hn' : n + a = n') : (0 : Cochain K L n).leftShift a n' hn' = 0 :=
  by
  change leftShiftAddEquiv K L n a n' hn' 0 = 0
  apply map_zero

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