feat: port Analysis.Convex.Star (#3050)

<!-- The text above the ` Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
leanprover-community · Mar 24, 2023 · e716737 · e716737
1 parent cf80a76
commit e716737
Show file tree

Hide file tree

Showing 2 changed files with 463 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -270,6 +270,7 @@ import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
 import Mathlib.Analysis.Convex.Segment
+import Mathlib.Analysis.Convex.Star
 import Mathlib.Analysis.Normed.Field.Basic
 import Mathlib.Analysis.Normed.Field.InfiniteSum
 import Mathlib.Analysis.Normed.Field.UnitBall