dotProduct_eq — Mathlib

English

If two vectors have the same dot product with every vector, then the vectors are equal.

Русский

Если два вектора дают одинаковое скалярное произведение с любым вектором, то сами вектора равны.

LaTeX

$$∀ {n} {R} [Semiring R] [Fintype n] (v w : n → R), (∀ u, dotProduct v u = dotProduct w u) → v = w$$

Lean4

theorem dotProduct_eq (v w : n → R) (h : ∀ u, v ⬝ᵥ u = w ⬝ᵥ u) : v = w :=
  by
  funext x
  classical rw [← dotProduct_single_one v x, ← dotProduct_single_one w x, h]

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