eq_zero_of_ortho — Mathlib

English

If M is nondegenerate and v orthogonal to all w with respect to M, then v = 0.

Русский

Если M невырожденная и для всех w выполняется v ⟂_M w, то v = 0.

LaTeX

$$$M \text{ nondegenerate } \Rightarrow (\forall v, (\forall w, v^T M w = 0) \Rightarrow v = 0)$$$

Lean4

/-- If `M` is nondegenerate and `w * M * v = 0` for all `w`, then `v = 0`. -/
theorem eq_zero_of_ortho {M : Matrix m m R} (hM : Nondegenerate M) {v : m → R} (hv : ∀ w, v ⬝ᵥ M *ᵥ w = 0) : v = 0 :=
  nondegenerate_def.mp hM v hv

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