gram_schmidt_ortho): Gram-Schmidt Orthogonalization and Orthonormalization (#12857)

Commit

3 years ago

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

Author

Biiiilly

Parents

92f6eb6b

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

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