Theorem InnerProductSpace.gramSchmidtNormed_linearIndependent

Modification history

2025-07-16 10:14
Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
feat: gramSchmidtNormed_linearIndependent and minor tweaks (#27023) …
Added InnerProductSpace.gramSchmidtNormed_linearIndependentView on Github →