Theorem orthogonal_projection_coe_linear_map_eq_linear_proj

Modification history

2023-03-16 17:03
src/analysis/inner_product_space/projection.lean
feat(analysis/inner_product_space/projection): express `orthogonal_projection` using `linear_proj_of_is_compl` (#18243) …
Added orthogonal_projection_coe_linear_map_eq_linear_projView on Github →