Theorem InnerProductSpace.gramSchmidt_bot

Modification history

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