Sort some imports alphabetically

leanprover-community · Aug 1, 2024 · 1d621d5 · 1d621d5
1 parent 02a630b
commit 1d621d5
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean
@@ -11,8 +11,8 @@ import Mathlib.Analysis.Normed.Module.Completion
 import Mathlib.Geometry.Manifold.Algebra.Monoid
 import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
 import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc
-import Mathlib.Geometry.Manifold.VectorBundle.Pullback
 import Mathlib.Geometry.Manifold.VectorBundle.Hom
+import Mathlib.Geometry.Manifold.VectorBundle.Pullback
 
 /-!
 # 1-jet bundles

diff --git a/SphereEversion/Local/DualPair.lean b/SphereEversion/Local/DualPair.lean
@@ -1,9 +1,9 @@
 import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
+import Mathlib.Analysis.Normed.Module.Completion
+import Mathlib.Data.Complex.Abs
 import Mathlib.LinearAlgebra.Dual
 import SphereEversion.Notations
 import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm.Prod
-import Mathlib.Data.Complex.Abs
-import Mathlib.Analysis.Normed.Module.Completion
 import SphereEversion.ToMathlib.LinearAlgebra.Basic
 
 /-! # Dual pairs

diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean
@@ -1,7 +1,7 @@
 import SphereEversion.InductiveConstructions
 import SphereEversion.Loops.Basic
-import SphereEversion.ToMathlib.ExistsOfConvex
 import SphereEversion.ToMathlib.Analysis.Normed.Module.FiniteDimension
+import SphereEversion.ToMathlib.ExistsOfConvex
 import SphereEversion.ToMathlib.SmoothBarycentric
 import SphereEversion.ToMathlib.Topology.Path
 import Mathlib.Analysis.Convex.Caratheodory