mathlib3

1a4df69c - feat(analysis/inner_product_space/basic): orthogonal submodules (#18705)

feat(analysis/inner_product_space/basic): orthogonal submodules (#18705) This adds `submodule.is_ortho U V`, with notation `U ⟂ V`, as a shorthand for `U ≤ Vᗮ`. To make this useful, this also adds about 30 lemmas of basic API. Some downstream proofs are golfed using the new API.