Theorem Matrix.star_dotProduct_gram_mulVec

Modification history

2025-12-19 07:43
Mathlib/Analysis/InnerProductSpace/GramMatrix.lean
chore: replace unnecessary `Fintype` hypotheses with `Finite` (#33068) …
Modified Matrix.star_dotProduct_gram_mulVecView on Github →
2025-10-11 15:08
Mathlib/Analysis/InnerProductSpace/GramMatrix.lean
feat: introduce Gram matrices (#25883) …
Added Matrix.star_dotProduct_gram_mulVecView on Github →