Theorem Matrix.posDef_gram_of_linearIndependent

Modification history

2025-10-11 15:08
Mathlib/Analysis/InnerProductSpace/GramMatrix.lean
feat: introduce Gram matrices (#25883) …
Added Matrix.posDef_gram_of_linearIndependentView on Github →