leftUnshift_zero — Mathlib

English

Relation-based formulation of leftShiftAddEquiv, relating the addition to the shift.

Русский

Реляционная формулировка leftShiftAddEquiv, связывающая сложение с сдвигом.

LaTeX

$$$\\text{LeftShiftAddEquiv}\\text{Rel}$$$

Lean4

@[simp]
theorem leftUnshift_zero (a n' : ℤ) (hn' : n + a = n') : (0 : Cochain (K⟦a⟧) L n').leftUnshift n hn' = 0 :=
  by
  change (leftShiftAddEquiv K L n a n' hn').symm 0 = 0
  apply map_zero

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