mathlib

e88badbf - feat(analysis/inner_product_space/pi_L2): Orthonormal basis (#12060)

feat(analysis/inner_product_space/pi_L2): Orthonormal basis (#12060) Added the structure orthonormal_basis and basic associated API Renamed the previous definition orthonormal_basis in analysis/inner_product_space/projection to std_orthonormal_basis Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>