chore: sort imports

[adomani]

Besides the sorting of the imports, this is what happens.

• LinearAlgebra/Charpoly/ToMatrix.lean:

  theorem charpoly_toMatrix uses set_option maxHeartbeats 400000 instead of 250000;

• NumberTheory/NumberField/Norm.lean:

  theorem isUnit_norm uses set_option maxHeartbeats 6400000 and synthInstance.maxHeartbeats 10000000 instead of nothing;

• Tactic/Positivity/Core.lean:

  import Mathlib.Tactic.NormNum.Core seems to have to be earlier than its alphabetic place, otherwise def normNumPositivity does not compile, even with increased (synth)Heartbeats.

Zulip discussion

---

[alexjbest]

!bench

[leanprover-bot]

Here are the benchmark results for commit 2ecf99b.
There were significant changes against commit 891adb3:

  Benchmark                                                                  Metric                Change
  =======================================================================================================
+ build                                                                      native compilation    -13.3%
- ~Mathlib.Algebra.Category.GroupCat.EpiMono                                 instructions            5.3%
- ~Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries   instructions            6.4%
+ ~Mathlib.Algebra.DirectSum.Finsupp                                         instructions           -6.8%
- ~Mathlib.Algebra.Homology.Homotopy                                         instructions            6.5%
- ~Mathlib.Algebra.Star.Subalgebra                                           instructions           17.7%
- ~Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps                 instructions           14.5%
+ ~Mathlib.Analysis.BoxIntegral.Basic                                        instructions           -5.6%
+ ~Mathlib.Analysis.BoxIntegral.DivergenceTheorem                            instructions          -12.4%
+ ~Mathlib.Analysis.Calculus.Deriv.Basic                                     instructions           -5.9%
+ ~Mathlib.Analysis.Calculus.Deriv.Linear                                    instructions          -11.9%
+ ~Mathlib.Analysis.Complex.ReImTopology                                     instructions           -5.1%
+ ~Mathlib.Analysis.NormedSpace.AffineIsometry                               instructions          -12.0%
- ~Mathlib.Analysis.NormedSpace.Algebra                                      instructions           13.3%
+ ~Mathlib.Analysis.NormedSpace.MatrixExponential                            instructions           -5.5%
- ~Mathlib.Analysis.NormedSpace.WeakDual                                     instructions           26.3%
+ ~Mathlib.Analysis.SpecialFunctions.Bernstein                               instructions           -6.5%
- ~Mathlib.CategoryTheory.Monad.Basic                                        instructions            5.9%
- ~Mathlib.CategoryTheory.Monoidal.Mod_                                      instructions            5.1%
+ ~Mathlib.CategoryTheory.Monoidal.Mon_                                      instructions           -7.9%
+ ~Mathlib.CategoryTheory.Sites.Closed                                       instructions           -6.7%
+ ~Mathlib.CategoryTheory.Sites.Spaces                                       instructions          -10.7%
- ~Mathlib.Combinatorics.HalesJewett                                         instructions           10.8%
- ~Mathlib.Data.Finsupp.Multiset                                             instructions           11.2%
+ ~Mathlib.Data.MvPolynomial.Equiv                                           instructions           -7.4%
+ ~Mathlib.Data.MvPolynomial.Supported                                       instructions          -14.6%
+ ~Mathlib.Data.MvPolynomial.Variables                                       instructions           -7.8%
- ~Mathlib.Data.Polynomial.Expand                                            instructions           73.9%
- ~Mathlib.Dynamics.BirkhoffSum.Average                                      instructions            5.4%
- ~Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber                  instructions            9.3%
+ ~Mathlib.Dynamics.Ergodic.Ergodic                                          instructions          -14.4%
+ ~Mathlib.Dynamics.Ergodic.MeasurePreserving                                instructions          -12.1%
+ ~Mathlib.FieldTheory.AxGrothendieck                                        instructions           -7.1%
- ~Mathlib.FieldTheory.Finite.GaloisField                                    instructions            5.8%
+ ~Mathlib.FieldTheory.IsSepClosed                                           instructions           -6.7%
- ~Mathlib.FieldTheory.Minpoly.Basic                                         instructions           31.2%
- ~Mathlib.Geometry.Manifold.Diffeomorph                                     instructions           20.3%
- ~Mathlib.Geometry.Manifold.PartitionOfUnity                                instructions            9.7%
- ~Mathlib.Geometry.Manifold.VectorBundle.Pullback                           instructions            5.5%
- ~Mathlib.Geometry.Manifold.WhitneyEmbedding                                instructions           85.2%
- ~Mathlib.LinearAlgebra.Charpoly.Basic                                      instructions           24.4%
- ~Mathlib.LinearAlgebra.Charpoly.ToMatrix                                   instructions           21.0%
- ~Mathlib.LinearAlgebra.Eigenspace.Minpoly                                  instructions            8.1%
+ ~Mathlib.LinearAlgebra.Finsupp                                             instructions           -8.9%
- ~Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff                               instructions            7.4%
- ~Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap                           instructions            8.7%
- ~Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly                             instructions           15.0%
+ ~Mathlib.LinearAlgebra.Matrix.Diagonal                                     instructions          -26.6%
+ ~Mathlib.LinearAlgebra.PID                                                 instructions           -7.9%
- ~Mathlib.LinearAlgebra.PiTensorProduct                                     instructions           11.8%
- ~Mathlib.LinearAlgebra.TensorPower                                         instructions            5.4%
- ~Mathlib.MeasureTheory.Function.AEMeasurableOrder                          instructions            8.3%
+ ~Mathlib.MeasureTheory.Function.SimpleFunc                                 instructions           -8.0%
+ ~Mathlib.MeasureTheory.Integral.DivergenceTheorem                          instructions           -8.9%
- ~Mathlib.MeasureTheory.Integral.RieszMarkovKakutani                        instructions           24.6%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                                instructions           -7.0%
+ ~Mathlib.MeasureTheory.Measure.OuterMeasure                                instructions          -12.7%
- ~Mathlib.MeasureTheory.Measure.Regular                                     instructions            5.5%
- ~Mathlib.ModelTheory.Basic                                                 instructions            6.1%
- ~Mathlib.NumberTheory.Cyclotomic.Basic                                     instructions            5.6%
- ~Mathlib.NumberTheory.NumberField.Basic                                    instructions            8.6%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding                       instructions          -36.8%
- ~Mathlib.NumberTheory.NumberField.Norm                                     instructions         1423.4%
+ ~Mathlib.Order.CompactlyGenerated                                          instructions          -13.6%
- ~Mathlib.Order.Filter.Lift                                                 instructions           14.4%
+ ~Mathlib.RepresentationTheory.Character                                    instructions           -5.3%
- ~Mathlib.RingTheory.Adjoin.FG                                              instructions            7.0%
+ ~Mathlib.RingTheory.AlgebraicIndependent                                   instructions          -10.3%
- ~Mathlib.RingTheory.Etale                                                  instructions           20.3%
- ~Mathlib.RingTheory.IntegralClosure                                        instructions            8.6%
+ ~Mathlib.RingTheory.Localization.Away.AdjoinRoot                           instructions          -21.4%
- ~Mathlib.RingTheory.Localization.NormTrace                                 instructions            5.7%
- ~Mathlib.RingTheory.Polynomial.Eisenstein.Basic                            instructions           10.8%
- ~Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral                       instructions            5.7%
+ ~Mathlib.RingTheory.Polynomial.Hermite.Gaussian                            instructions          -10.2%
- ~Mathlib.RingTheory.Polynomial.RationalRoot                                instructions           31.1%
- ~Mathlib.RingTheory.Polynomial.ScaleRoots                                  instructions           12.7%
- ~Mathlib.RingTheory.PowerSeries.Basic                                      instructions            5.8%
- ~Mathlib.RingTheory.PowerSeries.WellKnown                                  instructions            6.1%
+ ~Mathlib.RingTheory.TensorProduct                                          instructions           -7.8%
+ ~Mathlib.RingTheory.WittVector.IsPoly                                      instructions           -6.2%
+ ~Mathlib.RingTheory.WittVector.MulCoeff                                    instructions          -17.8%
+ ~Mathlib.RingTheory.WittVector.MulP                                        instructions          -11.6%
- ~Mathlib.Topology.Algebra.InfiniteSum.Module                               instructions           27.8%
- ~Mathlib.Topology.Algebra.Module.StrongTopology                            instructions            8.9%
- ~Mathlib.Topology.Algebra.StarSubalgebra                                   instructions           18.7%
- ~Mathlib.Topology.ContinuousFunction.Compact                               instructions           34.1%
- ~Mathlib.Topology.Homotopy.Basic                                           instructions           20.7%
- ~Mathlib.Topology.Order.LowerUpperTopology                                 instructions            7.5%
+ ~Mathlib.Topology.Sets.Closeds                                             instructions           -5.5%
+ ~Mathlib.Topology.Sets.Opens                                               instructions           -8.1%
+ ~Mathlib.Topology.Sheaves.PUnit                                            instructions           -8.1%
+ ~Mathlib.Topology.Sheaves.SheafCondition.Sites                             instructions          -18.4%
- ~Mathlib.Topology.UniformSpace.Equiv                                       instructions           11.3%
+ ~Mathlib.Topology.VectorBundle.Basic                                       instructions           -6.5%