Theorem Matrix.det_gram_ne_zero_iff_linearIndependent

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.det_gram_ne_zero_iff_linearIndependentView on Github →