feat: port Analysis.Convex.Basic (#3061)

Co-authored-by: Moritz Doll <moritz.doll@googlemail.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
leanprover-community · Mar 28, 2023 · 25d14ba · 25d14ba
1 parent f8741cb
commit 25d14ba
Show file tree

Hide file tree

Showing 3 changed files with 654 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -273,6 +273,7 @@ import Mathlib.Algebra.TrivSqZeroExt
 import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
+import Mathlib.Analysis.Convex.Basic
 import Mathlib.Analysis.Convex.Segment
 import Mathlib.Analysis.Convex.Star
 import Mathlib.Analysis.Normed.Field.Basic

diff --git a/Mathlib/Algebra/Order/Module.lean b/Mathlib/Algebra/Order/Module.lean
@@ -29,7 +29,7 @@ open Pointwise
 
 variable {k M N : Type _}
 
-instance [Semiring k] [OrderedAddCommMonoid M] [Module k M] : Module k Mᵒᵈ
+instance instModuleOrderDual [Semiring k] [OrderedAddCommMonoid M] [Module k M] : Module k Mᵒᵈ
     where
   add_smul _ _ x := OrderDual.rec (add_smul _ _) x
   zero_smul m := OrderDual.rec (zero_smul _) m