feat: port Analysis.NormedSpace.FiniteDimension (#4123)

leanprover-community · May 20, 2023 · 78acb82 · 78acb82
1 parent 3b22771
commit 78acb82
Show file tree

Hide file tree

Showing 2 changed files with 719 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -434,6 +434,7 @@ import Mathlib.Analysis.NormedSpace.ConformalLinearMap
 import Mathlib.Analysis.NormedSpace.ContinuousLinearMap
 import Mathlib.Analysis.NormedSpace.Extend
 import Mathlib.Analysis.NormedSpace.Extr
+import Mathlib.Analysis.NormedSpace.FiniteDimension
 import Mathlib.Analysis.NormedSpace.IndicatorFunction
 import Mathlib.Analysis.NormedSpace.Int
 import Mathlib.Analysis.NormedSpace.IsROrC