Commit 2022-04-20 10:04 8d351dc3

View on Github →

feat(analysis/inner_product_space/gram_schmidt_ortho): Gram-Schmidt Orthogonalization and Orthonormalization (#12857) Formalize Gram-Schmidt Orthogonalization and Orthonormalization

Estimated changes

Modified docs/undergrad.yaml

Created src/analysis/inner_product_space/gram_schmidt_ortho.lean

added theorem gram_schmidt_def'

added theorem gram_schmidt_def

added theorem gram_schmidt_ne_zero'

added theorem gram_schmidt_ne_zero

added theorem gram_schmidt_normed_unit_length'

added theorem gram_schmidt_normed_unit_length

added theorem gram_schmidt_orthogonal

added theorem gram_schmidt_orthonormal

added theorem gram_schmidt_pairwise_orthogonal

added theorem gram_schmidt_zero

added theorem span_gram_schmidt