Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-13 02:46 a2323660

View on Github →

feat(analysis/inner_product_space/projection): orthonormal basis subordinate to an orthogonal_family (#10208) In a finite-dimensional inner product space of E, there exists an orthonormal basis subordinate to a given direct sum decomposition into an orthogonal_family of subspaces E.

Estimated changes