vecMul_neg

Mathlib.Data.Matrix.Mul

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

English

Similarly, vecMul with a negated matrix equals the negation of vecMul with the original matrix.

Русский

Аналогично: v ᵥ* (-A) = -(v ᵥ* A).

LaTeX

$$$v ᵥ* (-A) = -(v ᵥ* A)$$$

Lean4

theorem vecMul_neg [Fintype m] (v : m → α) (A : Matrix m n α) : v ᵥ* (-A) = -(v ᵥ* A) :=
  by
  ext
  apply dotProduct_neg

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

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

Разделы

Аффилиация

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