sub_dotProduct

Mathlib.Data.Matrix.Mul

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

English

Distributivity of dot product over vector subtraction: u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w.

Русский

Равенство распределения скалярного произведения над разностью: u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w.

LaTeX

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

Lean4

@[simp]
theorem sub_dotProduct : (u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w := by simp [sub_eq_add_neg]

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

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

Разделы

Аффилиация

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