mathlib3

10f6c151 - chore(analysis/normed_space/inner_product): notation for orthogonal complement (#5536)

chore(analysis/normed_space/inner_product): notation for orthogonal complement (#5536) Notation for `submodule.orthogonal`, so that one can write `Kᗮ` instead of `K.orthogonal`. Simultaneous PR https://github.com/leanprover/vscode-lean/pull/246 adds `\perp` as vscode shorthand for this symbol. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/New.20linear.20algebra.20notation)