Commit 2022-10-05 21:07 96055b68

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.