Imports

leanprover-community · Feb 19, 2025 · acfb2fe · acfb2fe
1 parent 32166cf
commit acfb2fe
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Analysis/Normed/Module/Convex.lean b/Mathlib/Analysis/Normed/Module/Convex.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, Yury Kudryashov
 -/
 import Mathlib.Analysis.Convex.Jensen
-import Mathlib.Analysis.Normed.Module.Basic
 import Mathlib.Analysis.Convex.Topology
 import Mathlib.Analysis.Normed.Group.Pointwise
+import Mathlib.Analysis.Normed.Module.Basic
 
 /-!
 # Metric properties of convex sets in normed spaces