vec_neg

Mathlib.LinearAlgebra.Matrix.Vec

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

English

Vectorization commutes with negation: vec(-A) = -vec(A).

Русский

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

LaTeX

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

Lean4

theorem vec_neg [Neg R] (A : Matrix m n R) : vec (-A) = -vec A :=
  rfl

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

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

Разделы

Аффилиация

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