Commit 2023-04-04 16:43 1a4df69c
View on Github →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.