mathlib

82481e30 - feat(analysis/normed_space/inner_product): existence of orthonormal basis (#5734)

feat(analysis/normed_space/inner_product): existence of orthonormal basis (#5734) Define `orthonormal` sets (indexed) of vectors in an inner product space `E`. Show that a finite-dimensional inner product space has an orthonormal basis. Co-authored by: Busiso Chisala