Commit 2025-11-17 16:20 ecf19aa0
View on Github →feat(Analysis/InnerProductSpace/Orthogonal): map_orthogonal (#31728)
Add a lemma about mapping orthogonal complements under a LinearIsometryEquiv:
lemma map_orthogonal (f : E ≃ₗᵢ[𝕜] F) : Kᗮ.map f = (K.map f)ᗮ := by