Theorem orthogonal_projection_mem
Modification history
2020-12-22 17:05
src/analysis/normed_space/inner_product.lean
refactor(analysis/inner_product_space, geometry/euclidean) range of orthogonal projection (#5408) …
Deleted orthogonal_projection_memView on Github →