vec_sub

Mathlib.LinearAlgebra.Matrix.Vec

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

English

Vectorization commutes with subtraction: vec(A - B) = vec(A) - vec(B).

Русский

vec(A - B) = vec(A) - vec(B).

LaTeX

$$$$\operatorname{vec}(A - B) = \operatorname{vec}(A) - \operatorname{vec}(B)$$$$

Lean4

@[simp]
theorem vec_sub [Sub R] (A B : Matrix m n R) : vec (A - B) = vec A - vec B :=
  rfl

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

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

Разделы

Аффилиация

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