mathlib
a2d7a240 - Express `orthogonal_projection` as `linear_proj_of_is_compl`

Commit

3 years ago

Express `orthogonal_projection` as `linear_proj_of_is_compl`

References

#18041 - feat(analysis/inner_product_space/finite_dimensional): some lemmas on finite dimensional inner product spaces

#18290 - feat(analysis/von_neumann_algebra/basic): one result

Author

ADedecker

ADedecker

Parents

Loading