exists_not_ortho_of_ne_zero — Mathlib

English

If M is nondegenerate and v ≠ 0, then there exists w such that v^T M w ≠ 0.

Русский

Если M невырожденная и v ≠ 0, то существует w такое, что v^T M w ≠ 0.

LaTeX

$$$M.Nondegenerate \rightarrow (v \neq 0) \rightarrow \exists w, v^T M w \neq 0$$$

Lean4

/-- If `M` is nondegenerate and `v ≠ 0`, then there is some `w` such that `w * M * v ≠ 0`. -/
theorem exists_not_ortho_of_ne_zero {M : Matrix m m R} (hM : Nondegenerate M) {v : m → R} (hv : v ≠ 0) :
    ∃ w, v ⬝ᵥ M *ᵥ w ≠ 0 :=
  not_forall.mp (mt hM.eq_zero_of_ortho hv)

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