Theorem Matrix.linearIndependent_of_det_gram_ne_zero

Modification history

2026-04-14 17:36
Mathlib/Analysis/InnerProductSpace/GramMatrix.lean
feat(Analysis/InnerProductSpace): Gram matrix det ≠ 0 iff input vectors are independent (#37918) …
Added Matrix.linearIndependent_of_det_gram_ne_zeroView on Github →