Skip to content

Commit 34e8b42

Browse files
int-y1j-loreaux
andcommitted
feat: port Analysis.InnerProductSpace.Adjoint (#4476)
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
1 parent c639b48 commit 34e8b42

File tree

2 files changed

+545
-0
lines changed

2 files changed

+545
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -493,6 +493,7 @@ import Mathlib.Analysis.Convex.StrictConvexSpace
493493
import Mathlib.Analysis.Convex.Topology
494494
import Mathlib.Analysis.Convex.Uniform
495495
import Mathlib.Analysis.Hofer
496+
import Mathlib.Analysis.InnerProductSpace.Adjoint
496497
import Mathlib.Analysis.InnerProductSpace.Basic
497498
import Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
498499
import Mathlib.Analysis.InnerProductSpace.Dual

0 commit comments

Comments
 (0)