mathlib

95da6493 - feat(analysis/inner_product_space): Generalize Gram-Schmidt (#14379)

feat(analysis/inner_product_space): Generalize Gram-Schmidt (#14379) The generalisation is to allow a family of vectors indexed by a general indexing set `ι` (carrying appropriate order typeclasses) rather than just `ℕ`.