mathlib

fc5a82e1 - feat(analysis/inner_product/pi_L2): a finite orthonormal family is a basis of its span (#15481)

feat(analysis/inner_product/pi_L2): a finite orthonormal family is a basis of its span (#15481) We actually prove this for finite sub-families of a generic orthonormal basis because this is easier to use in practice