mathlib

96055b68 - feat(analysis/inner_product_space/gram_schmidt_ortho): generalize orthonormal basis construction (#16477)

feat(analysis/inner_product_space/gram_schmidt_ortho): generalize orthonormal basis construction (#16477) Previously, the construction `gram_schmidt_orthonormal_basis` performed Gram-Schmidt orthogonalization on an existing basis to produce an orthonormal basis. This changes it so that it outputs an orthonormal basis if the input is any family of vectors with the right sized index set. It augments the naive Gram-Schmidt output (an orthonormal-or-zero family of vectors, not necessarily spanning) arbitrarily to make an orthonormal basis. Formalized as part of the Sphere Eversion project.