mathlib

6e272cd8 - refactor(analysis/inner_product_space): split `submodule.orthogonal` to a new file (#18706)

refactor(analysis/inner_product_space): split `submodule.orthogonal` to a new file (#18706) This file is pretty long, and this seems to split out naturally. The lemmas are copied with minimal modification; the only change is that everything is now wrapped in `namespace submodule` rather than having `submodule.` prefixing every lemma.