dotProduct_neg

Mathlib.Data.Matrix.Mul

URI: https://scilib.ai/kg/mathlib#dotProduct_neg

English

The dot product is linear with respect to negation in the second argument: v ⬝ᵥ -w = -(v ⬝ᵥ w).

Русский

Скалярное произведение сохраняет отрицание во втором аргументе: v ⬝ᵥ -w = -(v ⬝ᵥ w).

LaTeX

$$$ v \cdot (-w) = -(v \cdot w) $$$

Lean4

@[simp]
theorem dotProduct_neg : v ⬝ᵥ -w = -(v ⬝ᵥ w) := by simp [dotProduct]

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

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

Разделы

Аффилиация

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