feat: port Analysis.NormedSpace.OperatorNorm (#3903)

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Arien Malec <arien.malec@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Mauricio Collares <mauricio@collares.org> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
leanprover-community · May 17, 2023 · 9ab4016 · 9ab4016
1 parent d995a93
commit 9ab4016
Show file tree

Hide file tree

Showing 4 changed files with 2,042 additions and 4 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -426,6 +426,7 @@ import Mathlib.Analysis.NormedSpace.IndicatorFunction
 import Mathlib.Analysis.NormedSpace.Int
 import Mathlib.Analysis.NormedSpace.LinearIsometry
 import Mathlib.Analysis.NormedSpace.MStructure
+import Mathlib.Analysis.NormedSpace.OperatorNorm
 import Mathlib.Analysis.NormedSpace.Pointwise
 import Mathlib.Analysis.NormedSpace.Ray
 import Mathlib.Analysis.NormedSpace.RieszLemma