Commit 2022-09-14 00:27 2ff92045

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.