vecMulVec_neg

Mathlib.Data.Matrix.Mul

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

English

The transpose of vecMulVec w v equals vecMulVec v w.

Русский

Транспонированная vecMulVec w v равна vecMulVec v w.

LaTeX

$$(vecMulVec w v)^{T} = vecMulVec v w$$

Lean4

@[simp]
theorem vecMulVec_neg [Mul α] [HasDistribNeg α] (w : m → α) (v : n → α) : vecMulVec w (-v) = -vecMulVec w v :=
  ext fun _ _ => mul_neg _ _

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

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

Разделы

Аффилиация

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