smul_vec2 — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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