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.