vec_smul

Mathlib.LinearAlgebra.Matrix.Vec

URI: https://scilib.ai/kg/mathlib#Matrix.vec_smul

English

Vectorization distributes over scalar multiplication: vec(r • A) = r • vec(A).

Русский

vec(r · A) = r · vec(A).

LaTeX

$$$$\operatorname{vec}(r \cdot A) = r \cdot \operatorname{vec}(A)$$$$

Lean4

@[simp]
theorem vec_smul {α} [SMul α R] (r : α) (A : Matrix m n R) : vec (r • A) = r • vec A :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru