mathlib3

67da2721 - feat(analysis/inner_product_space): Gram-Schmidt Basis (#14514)

feat(analysis/inner_product_space): Gram-Schmidt Basis (#14514) When the Gram-Schmidt procedure is given a basis, it produces a basis. This pull request also refactors the lemma `gram_schmidt_span`. The new versions of the lemmas cover the span of `Iio`, the span of `Iic` and the span of the complete set of input vectors. I was also able to remove some type classes in the process.