mathlib3
1313934b - feat(analysis/inner_product_space/l2_space): compute orthogonal projection on U given a hilbert basis of U (#15541)

Commit
3 years ago
feat(analysis/inner_product_space/l2_space): compute orthogonal projection on U given a hilbert basis of U (#15541)
Author
Parents
Loading