Theorems · Theorem · linear algebra

Matrix.Nondegenerate.eq_zero_of_ortho

∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Fintype m]
  [inst_2 : Fintype n], M.Nondegenerate → ∀ {v : m → R}, (∀ (w : n → R), v ⬝ᵥ M.mulVec w = 0) → v = 0

If M is nondegenerate and w * M * v = 0 for all w, then v = 0.

Defined in

Mathlib.LinearAlgebra.Matrix.Nondegenerate

Cited by

2 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringFintypeFintype