feat: port Analysis.InnerProductSpace.Adjoint (#4476)

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
leanprover-community · Jun 1, 2023 · 34e8b42 · 34e8b42
1 parent c639b48
commit 34e8b42
Show file tree

Hide file tree

Showing 2 changed files with 545 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -493,6 +493,7 @@ import Mathlib.Analysis.Convex.StrictConvexSpace
 import Mathlib.Analysis.Convex.Topology
 import Mathlib.Analysis.Convex.Uniform
 import Mathlib.Analysis.Hofer
+import Mathlib.Analysis.InnerProductSpace.Adjoint
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
 import Mathlib.Analysis.InnerProductSpace.Dual