rightUnshift_smul — Mathlib

English

The δ differential after a right shift relates to the δ of the original through a neg-one-power twist: δ n' m' (γ.rightShift a n' hn') = a.negOnePow · (δ n m γ).rightShift a m' hm'.

Русский

Диференциал δ после правого сдвига связан с δ исходного через множитель a.negOnePow: δ n' m' (γ.rightShift a n' hn') = a.negOnePow · (δ n m γ).rightShift a m' hm'.

LaTeX

$$$\delta n' m' (\gamma.rightShift a n' hn') = a.negOnePow · (\delta n m γ).rightShift a m' hm'$$$

Lean4

@[simp]
theorem rightUnshift_smul {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n) (x : R) :
    (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn :=
  by
  change (rightShiftLinearEquiv R K L n a n' hn).symm (x • γ) = _
  apply map_smul

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