neg_dotProduct_neg

Mathlib.Data.Matrix.Mul

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

English

The dot product is invariant under negating both vectors: (-v) ⬝ᵥ (-w) = v ⬝ᵥ w.

Русский

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

LaTeX

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

Lean4

theorem neg_dotProduct_neg : -v ⬝ᵥ -w = v ⬝ᵥ w := by rw [neg_dotProduct, dotProduct_neg, neg_neg]

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

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

Разделы

Аффилиация

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