kim-em · Oct 5, 2026 · Oct 5, 2026
diff --git a/Mathlib/Algebra/AddConstMap/Basic.lean b/Mathlib/Algebra/AddConstMap/Basic.lean
@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Group.Action.Pi
 public import Mathlib.Algebra.Group.End
 public import Mathlib.Algebra.Module.NatInt
 public import Mathlib.Algebra.Order.Archimedean.Basic
+
 import Mathlib.Algebra.Order.Group.Basic
 
 /-!

diff --git a/Mathlib/Algebra/AffineMonoid/Embedding.lean b/Mathlib/Algebra/AffineMonoid/Embedding.lean
@@ -6,11 +6,11 @@ Authors: Yaël Dillies, Patrick Luo
 module
 
 public import Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
+public import Mathlib.LinearAlgebra.Dimension.Free
 
 import Mathlib.Algebra.EuclideanDomain.Int
 import Mathlib.GroupTheory.MonoidLocalization.Finite
 import Mathlib.LinearAlgebra.FreeModule.PID
-public import Mathlib.LinearAlgebra.Dimension.Free
 
 /-!
 # Affine monoids embed into `ℤⁿ`

diff --git a/Mathlib/Algebra/Algebra/Spectrum/Pi.lean b/Mathlib/Algebra/Algebra/Spectrum/Pi.lean
@@ -6,6 +6,7 @@ Authors: Frédéric Dupuis
 module
 
 public import Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
+
 import Mathlib.Algebra.Group.Pi.Units
 
 /-!

diff --git a/Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean b/Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean
@@ -6,9 +6,10 @@ Authors: Jireh Loreaux
 module
 
 public import Mathlib.Algebra.Algebra.Spectrum.Basic
-import Mathlib.Algebra.Algebra.Tower
 public import Mathlib.Algebra.Algebra.Unitization
 
+import Mathlib.Algebra.Algebra.Tower
+
 /-!
 # Quasiregularity and quasispectrum
 

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/IsSimpleOrder.lean b/Mathlib/Algebra/Algebra/Subalgebra/IsSimpleOrder.lean
@@ -5,10 +5,11 @@ Authors: Kenny Lau
 -/
 module
 
-import Mathlib.LinearAlgebra.FiniteDimensional.Basic
 public import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
 public import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 
+import Mathlib.LinearAlgebra.FiniteDimensional.Basic
+
 /-!
 # Subalgebras of an algebra of prime dimension
 

diff --git a/Mathlib/Algebra/Algebra/Unitization.lean b/Mathlib/Algebra/Algebra/Unitization.lean
@@ -8,9 +8,10 @@ module
 public import Mathlib.Algebra.Star.Module
 public import Mathlib.Algebra.Star.StarProjection
 public import Mathlib.Algebra.Star.NonUnitalSubalgebra
-import Mathlib.Tactic.Abel
 public import Mathlib.Algebra.Module.TransferInstance
 
+import Mathlib.Tactic.Abel
+
 /-!
 # Unitization of a non-unital algebra
 

diff --git a/Mathlib/Algebra/AlgebraicCard.lean b/Mathlib/Algebra/AlgebraicCard.lean
@@ -5,9 +5,10 @@ Authors: Violeta Hernández Palacios
 -/
 module
 
-import Mathlib.Algebra.Polynomial.Cardinal
 public import Mathlib.RingTheory.Algebraic.Basic
 
+import Mathlib.Algebra.Polynomial.Cardinal
+
 /-!
 # Cardinality of algebraic numbers
 

diff --git a/Mathlib/Algebra/Azumaya/Basic.lean b/Mathlib/Algebra/Azumaya/Basic.lean
@@ -6,9 +6,10 @@ Authors: Yunzhou Xie, Jujian Zhang
 module
 
 public import Mathlib.Algebra.Azumaya.Defs
-import Mathlib.Algebra.Central.End
 public import Mathlib.Algebra.Central.TensorProduct
 
+import Mathlib.Algebra.Central.End
+
 /-!
 # Basic properties of Azumaya algebras
 

diff --git a/Mathlib/Algebra/BigOperators/Associated.lean b/Mathlib/Algebra/BigOperators/Associated.lean
@@ -6,9 +6,10 @@ Authors: Johannes Hölzl, Jens Wagemaker, Anne Baanen
 module
 
 public import Mathlib.Algebra.BigOperators.Finsupp.Basic
-import Mathlib.Algebra.Group.Submonoid.Membership
 public import Mathlib.Algebra.GroupWithZero.Associated
 
+import Mathlib.Algebra.Group.Submonoid.Membership
+
 /-!
 # Products of associated, prime, and irreducible elements.
 

diff --git a/Mathlib/Algebra/BigOperators/Expect.lean b/Mathlib/Algebra/BigOperators/Expect.lean
@@ -7,12 +7,12 @@ module
 
 public import Mathlib.Algebra.Algebra.Rat
 public import Mathlib.Algebra.BigOperators.GroupWithZero.Action
-import Mathlib.Algebra.BigOperators.Ring.Finset
 public import Mathlib.Algebra.Module.Pi
 public import Mathlib.Data.Finset.Density
 public import Mathlib.Data.Fintype.BigOperators
 public import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 
+import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Algebra.BigOperators.Group.Finset.Indicator
 
 /-!

diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Indicator.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Indicator.lean
@@ -7,9 +7,10 @@ module
 
 public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 public import Mathlib.Algebra.Group.Indicator
-import Mathlib.Data.Set.Lattice.Disjoint
 public import Mathlib.Order.CompleteLattice.Finset
 
+import Mathlib.Data.Set.Lattice.Disjoint
+
 /-!
 # Interaction of big operators with indicator functions
 -/

diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Interval.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Interval.lean
@@ -5,10 +5,11 @@ Authors: Chris Birkbeck
 -/
 module
 
-import Mathlib.Algebra.CharP.Defs
 public import Mathlib.Algebra.Group.EvenFunction
 public import Mathlib.Data.Int.Interval
 
+import Mathlib.Algebra.CharP.Defs
+
 /-!
 # Sums/products over integer intervals
 

diff --git a/Mathlib/Algebra/BigOperators/Group/List/Basic.lean b/Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@@ -5,7 +5,6 @@ Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
 module
 
-import Mathlib.Algebra.Divisibility.Basic
 public import Mathlib.Algebra.Group.Hom.Defs
 public import Mathlib.Algebra.BigOperators.Group.List.Defs
 public import Mathlib.Data.List.TakeDrop
@@ -17,6 +16,8 @@ public import Mathlib.Algebra.Group.Int.Defs
 public import Mathlib.Order.Basic
 public import Mathlib.Data.List.Basic
 
+import Mathlib.Algebra.Divisibility.Basic
+
 /-!
 # Sums and products from lists
 

diff --git a/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean b/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
@@ -6,6 +6,7 @@ Authors: Yury Kudryashov
 module
 
 public import Mathlib.Algebra.BigOperators.Finprod
+
 import Mathlib.Algebra.Group.Action.Basic
 import Mathlib.Algebra.Group.Units.Equiv
 

diff --git a/Mathlib/Algebra/BigOperators/Intervals.lean b/Mathlib/Algebra/BigOperators/Intervals.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
 public import Mathlib.Algebra.Order.Interval.Finset.Basic
 public import Mathlib.Algebra.Order.Sub.Basic
+
 import Mathlib.Data.Fintype.BigOperators
 
 /-!

diff --git a/Mathlib/Algebra/BigOperators/ModEq.lean b/Mathlib/Algebra/BigOperators/ModEq.lean
@@ -5,9 +5,10 @@ Authors: Yury Kudryashov
 -/
 module
 
-import Mathlib.Algebra.BigOperators.Ring.Finset
 public import Mathlib.Data.ZMod.Basic
 
+import Mathlib.Algebra.BigOperators.Ring.Finset
+
 /-!
 # Congruence modulo natural and integer numbers for big operators
 

diff --git a/Mathlib/Algebra/BigOperators/Ring/Nat.lean b/Mathlib/Algebra/BigOperators/Ring/Nat.lean
@@ -5,10 +5,11 @@ Authors: Pim Otte
 -/
 module
 
-import Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
 public import Mathlib.Data.Set.Finite.Lattice
 public import Mathlib.SetTheory.Cardinal.Finite
 
+import Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
+
 /-!
 # Big operators on a finset in the natural numbers
 

diff --git a/Mathlib/Algebra/BigOperators/RingEquiv.lean b/Mathlib/Algebra/BigOperators/RingEquiv.lean
@@ -6,9 +6,10 @@ Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 module
 
 public import Mathlib.Algebra.Ring.Equiv
-import Mathlib.Algebra.Ring.Opposite
 public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
 
+import Mathlib.Algebra.Ring.Opposite
+
 /-!
 # Results about mapping big operators across ring equivalences
 -/

diff --git a/Mathlib/Algebra/BrauerGroup/Defs.lean b/Mathlib/Algebra/BrauerGroup/Defs.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Category.AlgCat.Basic
 public import Mathlib.Algebra.Central.Defs
 public import Mathlib.LinearAlgebra.FiniteDimensional.Defs
+
 import Mathlib.LinearAlgebra.Matrix.Reindex
 
 /-!

diff --git a/Mathlib/Algebra/Category/AlgCat/FilteredColimits.lean b/Mathlib/Algebra/Category/AlgCat/FilteredColimits.lean
@@ -6,9 +6,10 @@ Authors: Christian Merten
 module
 
 public import Mathlib.Algebra.Category.AlgCat.Basic
-import Mathlib.Algebra.Category.Ring.Colimits
 public import Mathlib.Algebra.Category.Ring.FilteredColimits
 public import Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
+
+import Mathlib.Algebra.Category.Ring.Colimits
 import Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso
 
 /-!

diff --git a/Mathlib/Algebra/Category/AlgCat/TensorAlgebra.lean b/Mathlib/Algebra/Category/AlgCat/TensorAlgebra.lean
@@ -6,10 +6,11 @@ Authors: Christian Merten
 module
 
 public import Mathlib.Algebra.Category.AlgCat.Basic
+public import Mathlib.LinearAlgebra.TensorAlgebra.Basic
+
 import Mathlib.Algebra.Category.Grp.ZModuleEquivalence
 import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
 import Mathlib.Algebra.Ring.Shrink
-public import Mathlib.LinearAlgebra.TensorAlgebra.Basic
 
 /-!
 # `TensorAlgebra` as a functor `ModuleCat R ⥤ AlgCat R`

diff --git a/Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean b/Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean
@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Category.CoalgCat.Basic
 public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
 public import Mathlib.CategoryTheory.Monoidal.Comon_
 public import Mathlib.RingTheory.Coalgebra.TensorProduct
+
 import Mathlib.Tactic.SuppressCompilation
 
 /-!

diff --git a/Mathlib/Algebra/Category/FGModuleCat/Abelian.lean b/Mathlib/Algebra/Category/FGModuleCat/Abelian.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Category.FGModuleCat.Colimits
 public import Mathlib.Algebra.Category.FGModuleCat.Limits
 public import Mathlib.Algebra.Category.ModuleCat.Abelian
+
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
 
 /-!

diff --git a/Mathlib/Algebra/Category/FGModuleCat/Colimits.lean b/Mathlib/Algebra/Category/FGModuleCat/Colimits.lean
@@ -7,10 +7,11 @@ module
 
 public import Mathlib.Algebra.Category.FGModuleCat.Basic
 public import Mathlib.Algebra.Category.ModuleCat.Colimits
+public import Mathlib.LinearAlgebra.DirectSum.Finite
+
 import Mathlib.Algebra.Category.ModuleCat.EpiMono
 import Mathlib.Algebra.Category.ModuleCat.Products
 import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
-public import Mathlib.LinearAlgebra.DirectSum.Finite
 
 /-!
 # `forget₂ (FGModuleCat K) (ModuleCat K)` creates all finite colimits.

diff --git a/Mathlib/Algebra/Category/FGModuleCat/Limits.lean b/Mathlib/Algebra/Category/FGModuleCat/Limits.lean
@@ -6,9 +6,10 @@ Authors: Kim Morrison
 module
 
 public import Mathlib.Algebra.Category.FGModuleCat.Basic
-import Mathlib.Algebra.Category.ModuleCat.EpiMono
 public import Mathlib.Algebra.Category.ModuleCat.Limits
 public import Mathlib.Algebra.Category.ModuleCat.Products
+
+import Mathlib.Algebra.Category.ModuleCat.EpiMono
 import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
 
 /-!

diff --git a/Mathlib/Algebra/Category/Grp/AB.lean b/Mathlib/Algebra/Category/Grp/AB.lean
@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Category.Grp.Biproducts
 public import Mathlib.Algebra.Category.Grp.FilteredColimits
 public import Mathlib.Algebra.Homology.ShortComplex.Ab
 public import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
+
 import Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
 
 /-!

diff --git a/Mathlib/Algebra/Category/Grp/Adjunctions.lean b/Mathlib/Algebra/Category/Grp/Adjunctions.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Category.Grp.Preadditive
 public import Mathlib.GroupTheory.FreeAbelianGroup
+
 import Mathlib.CategoryTheory.Adjunction.Limits
 import Mathlib.CategoryTheory.Limits.Types.Coproducts
 

diff --git a/Mathlib/Algebra/Category/Grp/EnoughInjectives.lean b/Mathlib/Algebra/Category/Grp/EnoughInjectives.lean
@@ -6,6 +6,7 @@ Authors: Jujian Zhang, Junyan Xu
 module
 
 public import Mathlib.Algebra.Module.CharacterModule
+
 import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
 import Mathlib.Algebra.Category.Grp.EpiMono
 

diff --git a/Mathlib/Algebra/Category/Grp/EpiMono.lean b/Mathlib/Algebra/Category/Grp/EpiMono.lean
@@ -6,11 +6,12 @@ Authors: Jujian Zhang
 module
 
 public import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
-import Mathlib.CategoryTheory.ConcreteCategory.EpiMono
 public import Mathlib.CategoryTheory.Limits.Constructions.EpiMono
 public import Mathlib.GroupTheory.Coset.Basic
 public import Mathlib.GroupTheory.QuotientGroup.Defs
 
+import Mathlib.CategoryTheory.ConcreteCategory.EpiMono
+
 /-!
 # Monomorphisms and epimorphisms in `Group`
 

diff --git a/Mathlib/Algebra/Category/Grp/IsFinite.lean b/Mathlib/Algebra/Category/Grp/IsFinite.lean
@@ -5,10 +5,11 @@ Authors: Joël Riou
 -/
 module
 
-import Mathlib.Algebra.Category.Grp.Zero
 public import Mathlib.Algebra.Homology.ShortComplex.Ab
 public import Mathlib.CategoryTheory.Abelian.SerreClass.Basic
 
+import Mathlib.Algebra.Category.Grp.Zero
+
 /-!
 # The Serre class of finite abelian groups
 

diff --git a/Mathlib/Algebra/Category/Grp/LargeColimits.lean b/Mathlib/Algebra/Category/Grp/LargeColimits.lean
@@ -6,6 +6,7 @@ Authors: Sophie Morel
 module
 
 public import Mathlib.Algebra.Category.Grp.Colimits
+
 import Mathlib.Algebra.Module.CharacterModule
 
 /-!

diff --git a/Mathlib/Algebra/Category/Grp/Subobject.lean b/Mathlib/Algebra/Category/Grp/Subobject.lean
@@ -5,9 +5,10 @@ Authors: Markus Himmel
 -/
 module
 
-import Mathlib.Algebra.Category.Grp.ZModuleEquivalence
 public import Mathlib.Algebra.Category.ModuleCat.Subobject
 
+import Mathlib.Algebra.Category.Grp.ZModuleEquivalence
+
 /-!
 # The category of abelian groups is well-powered
 -/

diff --git a/Mathlib/Algebra/Category/ModuleCat/AB.lean b/Mathlib/Algebra/Category/ModuleCat/AB.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Category.Grp.AB
 public import Mathlib.Algebra.Category.ModuleCat.Colimits
+
 import Mathlib.Algebra.Module.Shrink
 /-!
 

diff --git a/Mathlib/Algebra/Category/ModuleCat/EnoughInjectives.lean b/Mathlib/Algebra/Category/ModuleCat/EnoughInjectives.lean
@@ -6,6 +6,7 @@ Authors: Jujian Zhang
 module
 
 public import Mathlib.Algebra.Category.Grp.EnoughInjectives
+
 import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
 import Mathlib.Algebra.Ring.Shrink
 

diff --git a/Mathlib/Algebra/Category/ModuleCat/Ext/Baer.lean b/Mathlib/Algebra/Category/ModuleCat/Ext/Baer.lean
@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Category.ModuleCat.EnoughInjectives
 public import Mathlib.Algebra.Category.ModuleCat.Ext.HasExt
 public import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
 public import Mathlib.CategoryTheory.Abelian.Injective.Dimension
+
 import Mathlib.CategoryTheory.Abelian.Injective.Resolution
 
 /-!

diff --git a/Mathlib/Algebra/Category/ModuleCat/Ext/DimensionShifting.lean b/Mathlib/Algebra/Category/ModuleCat/Ext/DimensionShifting.lean
@@ -6,12 +6,13 @@ Authors: Nailin Guan
 module
 
 public import Mathlib.Algebra.Category.ModuleCat.Ext.HasExt
-import Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
 public import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
 public import Mathlib.Data.Nat.Totient
 public import Mathlib.Data.Rat.Floor
 public import Mathlib.Tactic.Continuity
 
+import Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
+
 /-!
 
 # Dimension Shifting
-Original file line number
+Diff line change
@@ Expand Up / @@ -6,6 +6,7 @@ Authors: Frédéric Dupuis @@
     module
     public import Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
     import Mathlib.Algebra.Group.Pi.Units
     /-!
@@ Expand Down @@