shift_neg — Mathlib

English

Let a be an integer. For any cochain γ, negating γ and then shifting by a equals shifting γ by a and then negating: (-γ).shift a = - (γ.shift a).

Русский

Пусть a — целое число. Любой косоценный γ удовлетворяет: (-γ).shift a = - (γ.shift a).

LaTeX

$$$(-\gamma).shift a = -\gamma.shift a$$$

Lean4

@[simp]
theorem shift_neg (a : ℤ) : (-γ).shift a = -γ.shift a :=
  by
  change shiftAddHom K L n a (-γ) = _
  apply map_neg

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