Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-16 19:20 67da2721

View on Github →

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.

Estimated changes

Modified src/analysis/inner_product_space/gram_schmidt_ortho.lean

added theorem coe_gram_schmidt_basis

added theorem gram_schmidt_linear_independent

added theorem gram_schmidt_mem_span

modified theorem gram_schmidt_ne_zero

modified theorem gram_schmidt_ne_zero_coe

modified theorem gram_schmidt_normed_unit_length

modified theorem gram_schmidt_normed_unit_length_coe

modified theorem gram_schmidt_orthonormal

added theorem gram_schmidt_triangular

modified theorem gram_schmidt_zero

added theorem mem_span_gram_schmidt

modified theorem span_gram_schmidt

added theorem span_gram_schmidt_Iic

added theorem span_gram_schmidt_Iio

added theorem span_gram_schmidt_normed

added theorem span_gram_schmidt_normed_range

Modified src/linear_algebra/span.lean

added theorem submodule.span_eq_span