mathlib

a2323660 - feat(analysis/inner_product_space/projection): orthonormal basis subordinate to an `orthogonal_family` (#10208)

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`.