shift_smul — Mathlib

English

Shift interacts linearly with scalar multiplication: shift_smul (a, x) gives (x γ).shift a = x (γ.shift a).

Русский

Сдвиг линейно взаимодействует со скалярным умножением: shift_smul (a, x) дает (x γ).shift a = x (γ.shift a).

LaTeX

$$$(x \cdot \gamma).shift a = x \cdot (\gamma.shift a)$$$

Lean4

@[simp]
theorem shift_smul (a : ℤ) (x : R) : (x • γ).shift a = x • (γ.shift a) :=
  by
  ext p q hpq
  dsimp
  simp only [shift_v', smul_v]

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