Theorem Submodule.map_orthogonal_equiv

Modification history

2026-01-21 00:52
Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
feat(Geometry/Euclidean/Altitude): `map` and `restrict` lemmas (#32021) …
Added Submodule.map_orthogonal_equivView on Github →