Commit 2023-03-30 17:06 6e272cd8

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.