Theorem InnerProductSpace.gramSchmidtOrthonormalBasis_inv_blockTriangular

Modification history

2026-07-30 16:24
Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
feat(LinearAlgebra/Matrix): add definitions and theory for the echelon form and pivots of matrices (#42236) …
Deleted InnerProductSpace.gramSchmidtOrthonormalBasis_inv_blockTriangularView on Github →
2025-07-10 19:37
Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
chore(Gram-Schmidt): small tweaks (#26894) …
Added InnerProductSpace.gramSchmidtOrthonormalBasis_inv_blockTriangularView on Github →