rightUnshift_neg — Mathlib

English

RightUnshift commutes with negation: (-γ).rightUnshift n hn = - (γ.rightUnshift n hn).

Русский

RightUnshift сохраняет знак: (-γ).rightUnshift n hn = -(γ.rightUnshift n hn).

LaTeX

$$$(-\\gamma).rightUnshift n hn = - (\\gamma.rightUnshift n hn)$$$

Lean4

@[simp]
theorem rightUnshift_neg {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n) :
    (-γ).rightUnshift n hn = -γ.rightUnshift n hn :=
  by
  change (rightShiftAddEquiv K L n a n' hn).symm (-γ) = _
  apply map_neg

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