mathlib3

22f57723 - feat(analysis/inner_product_space/projection): express `orthogonal_projection` using `linear_proj_of_is_compl` (#18243)

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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>