Commit 2023-03-16 17:03 22f57723
View on Github →feat(analysis/inner_product_space/projection): express orthogonal_projection using linear_proj_of_is_compl (#18243)
We currently don't have any link between orthogonal_projection and linear_proj_of_is_compl, which blocks us from applying general algebraic facts about projection to orthogonal_projection. This PR fixes that.