feat: port Analysis.LocallyConvex.Basic (#3398)

leanprover-community · Apr 12, 2023 · 344196c · 344196c
1 parent 230c1dc
commit 344196c
Show file tree

Hide file tree

Showing 2 changed files with 436 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -298,6 +298,7 @@ import Mathlib.Analysis.Convex.Slope
 import Mathlib.Analysis.Convex.Star
 import Mathlib.Analysis.Convex.Strict
 import Mathlib.Analysis.Hofer
+import Mathlib.Analysis.LocallyConvex.Basic
 import Mathlib.Analysis.LocallyConvex.Polar
 import Mathlib.Analysis.Normed.Field.Basic
 import Mathlib.Analysis.Normed.Field.InfiniteSum