mathlib3

2ff92045 - feat(analysis/inner_product_space/projection): remove useless `complete_space E` assumption (#15682)

feat(analysis/inner_product_space/projection): remove useless `complete_space E` assumption (#15682) The current proof decomposes v as its projection on K and its projection on the orthogonal complement of K, thus requiring `E` to be complete. Instead, we decompose it as `v = p v + (v - p v)`, where `p` is the projection on K.