mathlib

72252b3c - feat(analysis/inner_product_space/projection): norm_sq_eq_sum_norm_sq… (#12096)

feat(analysis/inner_product_space/projection): norm_sq_eq_sum_norm_sq… (#12096) …_projection The Pythagorean theorem for an orthogonal projection onto a submodule S. I am sure that there are some style changes that could/should be made! Co-authored-by: Daniel Packer Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com>