feat: port Analysis.NormedSpace.BoundedLinearMaps (#4091)

Simplify a few proofs to avoid non-terminal simps in favor of rewrites and `have` instead of `convert`.
leanprover-community · May 20, 2023 · 3310935 · 3310935
1 parent b58077e
commit 3310935
Show file tree

Hide file tree

Showing 2 changed files with 653 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -431,6 +431,7 @@ import Mathlib.Analysis.NormedSpace.BallAction
 import Mathlib.Analysis.NormedSpace.Banach
 import Mathlib.Analysis.NormedSpace.BanachSteinhaus
 import Mathlib.Analysis.NormedSpace.Basic
+import Mathlib.Analysis.NormedSpace.BoundedLinearMaps
 import Mathlib.Analysis.NormedSpace.CompactOperator
 import Mathlib.Analysis.NormedSpace.Complemented
 import Mathlib.Analysis.NormedSpace.Completion