Theorem Submodule.map_orthogonal

Modification history

2026-01-21 00:52
Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
feat(Geometry/Euclidean/Altitude): `map` and `restrict` lemmas (#32021) …
Modified Submodule.map_orthogonalView on Github →
2025-12-27 09:40
Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
chore(*): restrict operations to `LinearMap`s (#33241) …
Modified Submodule.map_orthogonalView on Github →
2025-11-17 16:20
Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
feat(Analysis/InnerProductSpace/Orthogonal): `map_orthogonal` (#31728) …
Added Submodule.map_orthogonalView on Github →