leftShift_smul — Mathlib

English

Scalar multiplication commutes with the left shift: (x γ).leftShift a n' hn' = x γ.leftShift a n' hn'.

Русский

Скалярное умножение и левый сдвиг коммутируют: (x γ).leftShift a n' hn' = x γ.leftShift a n' hn'.

LaTeX

$$$(x \cdot \gamma).leftShift a n' hn' = x \cdot (\gamma.leftShift a n' hn')$$$

Lean4

@[simp]
theorem leftShift_smul (a n' : ℤ) (hn' : n + a = n') (x : R) : (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn' :=
  by
  ext p q hpq
  dsimp
  simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by cutsat), smul_v, Linear.comp_smul, smul_comm x]

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