smul_vec3 — Mathlib

English

Scalar multiplication distributes over a 3-element vector: x • [a0,a1,a2] = [x•a0, x•a1, x•a2].

Русский

Умножение на скаляр распределяется по компонентам вектора 3 элементов: x • [a0,a1,a2] = [x•a0, x•a1, x•a2].

LaTeX

$$$x \cdot \begin{pmatrix} a_0 \\ a_1 \\ a_2 \end{pmatrix} = \begin{pmatrix} x \cdot a_0 \\ x \cdot a_1 \\ x \cdot a_2 \end{pmatrix}$$$

Lean4

theorem smul_vec3 {R : Type*} [SMul R α] (x : R) (a₀ a₁ a₂ : α) : x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂] := by
  simp

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