dotProduct_eq_zero

Mathlib.LinearAlgebra.Matrix.DotProduct

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

English

Let v be a vector in R^n. If v · w = 0 for every w in R^n, then v = 0.

Русский

Пусть v — вектор в R^n. Если для каждого w в R^n скалярное произведение v · w равно нулю, то v = 0.

LaTeX

$$(∀ w: n → R, v · w = 0) ⇒ v = 0$$

Lean4

theorem dotProduct_eq_zero (v : n → R) (h : ∀ w, v ⬝ᵥ w = 0) : v = 0 :=
  dotProduct_eq _ _ fun u => (h u).symm ▸ (zero_dotProduct u).symm

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

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

Разделы

Аффилиация

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