leanprover-community · harahu · May 20, 2026 · May 20, 2026
diff --git a/Mathlib/Algebra/Algebra/RestrictScalars.lean b/Mathlib/Algebra/Algebra/RestrictScalars.lean
@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Algebra.Tower
 
 /-!
-
 # The `RestrictScalars` type alias
 
 See the documentation attached to the `RestrictScalars` definition for advice on how and when to

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/MulOpposite.lean b/Mathlib/Algebra/Algebra/Subalgebra/MulOpposite.lean
@@ -9,7 +9,6 @@ public import Mathlib.Algebra.Algebra.Subalgebra.Lattice
 public import Mathlib.Algebra.Ring.Subring.MulOpposite
 
 /-!
-
 # Subalgebras of opposite rings
 
 For every ring `A` over a commutative ring `R`, we construct an equivalence between

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean b/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean
@@ -10,7 +10,6 @@ public import Mathlib.LinearAlgebra.Dimension.Subsingleton
 public import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 
 /-!
-
 # Some results on the ranks of subalgebras
 
 This file contains some results on the ranks of subalgebras,

diff --git a/Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean b/Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean
diff --git a/Mathlib/Algebra/Category/Grp/EnoughInjectives.lean b/Mathlib/Algebra/Category/Grp/EnoughInjectives.lean
@@ -11,7 +11,6 @@ public import Mathlib.Algebra.Category.Grp.EpiMono
 public import Mathlib.Algebra.Category.Grp.Injective
 
 /-!
-
 # Category of abelian groups has enough injectives
 
 Given an abelian group `A`, then `i : A ⟶ ∏_{A⋆} ℚ ⧸ ℤ` defined by `i : a ↦ c ↦ c a` is an

diff --git a/Mathlib/Algebra/Category/Grp/FiniteGrp.lean b/Mathlib/Algebra/Category/Grp/FiniteGrp.lean
@@ -9,7 +9,6 @@ public import Mathlib.Data.Finite.Defs
 public import Mathlib.Algebra.Category.Grp.Basic
 
 /-!
-
 ## Main definitions and results
 
 * `FiniteGrp` is the category of finite groups.

diff --git a/Mathlib/Algebra/Category/ModuleCat/AB.lean b/Mathlib/Algebra/Category/ModuleCat/AB.lean
@@ -10,7 +10,6 @@ public import Mathlib.Algebra.Category.ModuleCat.Colimits
 public import Mathlib.Algebra.Module.Shrink
 public import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
 /-!
-
 # AB axioms in module categories
 
 This file proves that the category of modules over a ring satisfies Grothendieck's axioms AB5, AB4,

diff --git a/Mathlib/Algebra/Category/ModuleCat/Ext/DimensionShifting.lean b/Mathlib/Algebra/Category/ModuleCat/Ext/DimensionShifting.lean
@@ -13,7 +13,6 @@ public import Mathlib.Data.Rat.Floor
 public import Mathlib.Tactic.Continuity
 
 /-!
-
 # Dimension Shifting
 
 -/

diff --git a/Mathlib/Algebra/Category/ModuleCat/Ext/Finite.lean b/Mathlib/Algebra/Category/ModuleCat/Ext/Finite.lean
@@ -11,7 +11,6 @@ public import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
 public import Mathlib.RingTheory.Noetherian.Basic
 
 /-!
-
 # `Ext`-modules between finitely generated modules over Noetherian rings are finitely generated
 
 -/

diff --git a/Mathlib/Algebra/Category/ModuleCat/Ext/HasExt.lean b/Mathlib/Algebra/Category/ModuleCat/Ext/HasExt.lean
@@ -9,7 +9,6 @@ public import Mathlib.Algebra.Category.ModuleCat.Projective
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
 
 /-!
-
 # HasExt instance for Module Category
 
 If we assume `Small.{v} R`, the category `ModuleCat.{v} R` has enough projectives, which allows to

diff --git a/Mathlib/Algebra/Category/ModuleCat/Localization.lean b/Mathlib/Algebra/Category/ModuleCat/Localization.lean
@@ -11,7 +11,6 @@ public import Mathlib.Algebra.Module.LocalizedModule.Exact
 public import Mathlib.RingTheory.Localization.Module
 
 /-!
-
 # Localized Module in ModuleCat
 
 For a ring `R` satisfying `[Small.{v} R]` and a submonoid `S` of `R`,

diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
@@ -17,7 +17,6 @@ An object `M : PresheafOfModules R` consists of a family of modules
 of a functorial linear map `M.map f` from `M.obj X` to the restriction
 of scalars of `M.obj Y` via `R.map f`.
 
-
 ## Future work
 
 * Compare this to the definition as a presheaf of pairs `(R, M)` with specified first part.

diff --git a/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean b/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean
@@ -11,7 +11,6 @@ public import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
 public import Mathlib.CategoryTheory.Abelian.Projective.Dimension
 
 /-!
-
 # Projective Dimension in ModuleCat
 
 -/

diff --git a/Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean b/Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean
@@ -11,7 +11,6 @@ public import Mathlib.Algebra.Homology.ShortComplex.Abelian
 public import Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
 
 /-!
-
 # `TopModuleCat` is a `CategoryWithHomology`
 
 `TopModuleCat R`, the category of topological `R`-modules, is not an abelian category.

diff --git a/Mathlib/Algebra/Category/ModuleCat/Ulift.lean b/Mathlib/Algebra/Category/ModuleCat/Ulift.lean
@@ -13,7 +13,6 @@ public import Mathlib.CategoryTheory.Preadditive.Injective.Preserves
 public import Mathlib.CategoryTheory.Preadditive.Projective.Preserves
 
 /-!
-
 # Ulift functor for ModuleCat
 
 In this file, we define the obvious functor `ModuleCat.{v} R ⥤ ModuleCat.{max v v'} R` and prove

diff --git a/Mathlib/Algebra/Category/Ring/FinitePresentation.lean b/Mathlib/Algebra/Category/Ring/FinitePresentation.lean
@@ -13,7 +13,6 @@ public import Mathlib.RingTheory.EssentialFiniteness
 public import Mathlib.RingTheory.FinitePresentation
 
 /-!
-
 # Finitely presentable objects in `Under R` with `R : CommRingCat`
 
 In this file, we show that finitely presented algebras are finitely presentable in `Under R`,

diff --git a/Mathlib/Algebra/Central/TensorProduct.lean b/Mathlib/Algebra/Central/TensorProduct.lean
@@ -10,7 +10,6 @@ public import Mathlib.RingTheory.Flat.Basic
 public import Mathlib.LinearAlgebra.Basis.VectorSpace
 
 /-!
-
 # Lemmas about tensor products of central algebras
 
 In this file we prove for algebras `B` and `C` over a field `K` that if `B ⊗[K] C` is a central

diff --git a/Mathlib/Algebra/CharP/Algebra.lean b/Mathlib/Algebra/CharP/Algebra.lean
@@ -18,7 +18,6 @@ In this file we describe the characteristic of `R`-algebras.
 In particular we are interested in the characteristic of free algebras over `R`
 and the fraction field `FractionRing R`.
 
-
 ## Main results
 
 - `charP_of_injective_algebraMap` If `R →+* A` is an injective algebra map

diff --git a/Mathlib/Algebra/CharP/IntermediateField.lean b/Mathlib/Algebra/CharP/IntermediateField.lean
@@ -9,7 +9,6 @@ public import Mathlib.Algebra.CharP.Algebra
 public import Mathlib.FieldTheory.IntermediateField.Basic
 
 /-!
-
 # Characteristic of intermediate fields
 
 This file contains some convenient instances for determining the characteristic of

diff --git a/Mathlib/Algebra/CharZero/Defs.lean b/Mathlib/Algebra/CharZero/Defs.lean
@@ -9,7 +9,6 @@ public import Mathlib.Data.Int.Cast.Defs
 public import Mathlib.Logic.Basic
 
 /-!
-
 # Characteristic zero
 
 A ring `R` is called of characteristic zero if every natural number `n` is non-zero when considered

diff --git a/Mathlib/Algebra/DirectSum/Decomposition.lean b/Mathlib/Algebra/DirectSum/Decomposition.lean
@@ -17,7 +17,6 @@ public import Mathlib.Algebra.Module.Submodule.Basic
   an additive monoid `M` into a family of additive submonoids `ℳ`
 * `DirectSum.decompose ℳ`: The canonical equivalence provided by the above typeclass
 
-
 ## Main statements
 
 * `DirectSum.Decomposition.isInternal`: The link to `DirectSum.IsInternal`.

diff --git a/Mathlib/Algebra/EuclideanDomain/Defs.lean b/Mathlib/Algebra/EuclideanDomain/Defs.lean
@@ -55,7 +55,6 @@ value of `j`.
   [MR399081]
 * [M. Nagata, *On Euclid algorithm*][MR541021]
 
-
 ## Tags
 
 Euclidean domain, transfinite Euclidean domain, Bézout's lemma

diff --git a/Mathlib/Algebra/GCDMonoid/IntegrallyClosed.lean b/Mathlib/Algebra/GCDMonoid/IntegrallyClosed.lean
@@ -10,7 +10,6 @@ public import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
 public import Mathlib.RingTheory.Polynomial.Eisenstein.Basic
 
 /-!
-
 # GCD domains are integrally closed
 
 -/

diff --git a/Mathlib/Algebra/Group/Indicator.lean b/Mathlib/Algebra/Group/Indicator.lean
@@ -18,7 +18,6 @@ In this file, we prove basic results about the indicator of a set.
 - `Set.indicator (s : Set α) (f : α → β) (a : α)` is `f a` if `a ∈ s` and is `0` otherwise.
 - `Set.mulIndicator (s : Set α) (f : α → β) (a : α)` is `f a` if `a ∈ s` and is `1` otherwise.
 
-
 ## Implementation note
 
 In mathematics, an indicator function or a characteristic function is a function

diff --git a/Mathlib/Algebra/Group/Submonoid/Units.lean b/Mathlib/Algebra/Group/Submonoid/Units.lean
@@ -10,7 +10,6 @@ public import Mathlib.Algebra.Group.Submonoid.Pointwise
 public import Mathlib.Algebra.Group.Subgroup.Lattice
 
 /-!
-
 # Submonoid of units
 
 Given a submonoid `S` of a monoid `M`, we define the subgroup `S.units` as the units of `S` as a

diff --git a/Mathlib/Algebra/GroupWithZero/Hom.lean b/Mathlib/Algebra/GroupWithZero/Hom.lean
@@ -16,7 +16,6 @@ This file defines homomorphisms of monoids with zero.
 We also define coercion to a function, and usual operations: composition, identity homomorphism,
 pointwise multiplication and pointwise inversion.
 
-
 ## Notation
 
 * `→*₀`: `MonoidWithZeroHom`, the type of bundled `MonoidWithZero` homs. Also use for

diff --git a/Mathlib/Algebra/Homology/DerivedCategory/Ext/MapBijective.lean b/Mathlib/Algebra/Homology/DerivedCategory/Ext/MapBijective.lean
@@ -14,7 +14,6 @@ public import Mathlib.CategoryTheory.Preadditive.Injective.Preserves
 public import Mathlib.CategoryTheory.Preadditive.Projective.Preserves
 
 /-!
-
 # Bijections Between Ext
 
 In this file, we show that the maps between `Ext` induced

diff --git a/Mathlib/Algebra/Lie/Derivation/BaseChange.lean b/Mathlib/Algebra/Lie/Derivation/BaseChange.lean
@@ -16,7 +16,6 @@ When, given an `R`-algebra `A` and an `R`-Lie algebra `L` the (Lie algebra) base
 both derivations of `A` and Lie derivations of `L` induce Lie derivations of `A ⊗[R] L`. Moreover,
 both these procedures are Lie algebra homomorphisms themselves.
 
-
 ## Tags
 
 lie algebra, extension of scalars, base change, derivation

diff --git a/Mathlib/Algebra/Lie/SemiDirect.lean b/Mathlib/Algebra/Lie/SemiDirect.lean
@@ -19,7 +19,6 @@ algebra homomorphism  `ψ : L → LieDerivation  R K K`, the underlying set of t
 itself a Lie algebra and that it fits into an exact sequence `H → (SemiDirectSum K L ψ) → L`, i.e.
 forms an extension of `L`.
 
-
 ## References
 
 * https://en.wikipedia.org/wiki/Lie_algebra_extension#By_semidirect_sum

diff --git a/Mathlib/Algebra/Lie/Sl2.lean b/Mathlib/Algebra/Lie/Sl2.lean
@@ -11,7 +11,6 @@ public import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 public import Mathlib.Algebra.Lie.Weights.Basic
 
 /-!
-
 # The Lie algebra `sl₂` and its representations
 
 The Lie algebra `sl₂` is the unique simple Lie algebra of minimal rank, 1, and as such occupies a

diff --git a/Mathlib/Algebra/Module/FinitePresentation.lean b/Mathlib/Algebra/Module/FinitePresentation.lean
@@ -14,7 +14,6 @@ public import Mathlib.RingTheory.Noetherian.Basic
 public import Mathlib.RingTheory.TensorProduct.Finite
 
 /-!
-
 # Finitely Presented Modules
 
 ## Main definition
@@ -37,7 +36,6 @@ Suppose `0 → K → M → N → 0` is an exact sequence of `R`-modules.
 - `Module.FinitePresentation.isLocalizedModule_map`: If `M` and `N` are `R`-modules and `M` is f.p.,
   and `S` is a submonoid of `R`, then `Hom(Mₛ, Nₛ)` is the localization of `Hom(M, N)`.
 
-
 Also the instances finite + free => f.p. => finite are also provided
 
 ## TODO
@@ -50,7 +48,6 @@ Suppose `S` is an `R`-algebra, `M` is an `S`-module. Then
 In particular,
 4. `S` is f.p. as an `R`-module iff it is f.p. as an algebra and is finite as a module.
 
-
 For finitely presented algebras, see `Algebra.FinitePresentation`
 in file `Mathlib/RingTheory/FinitePresentation.lean`.
 -/

diff --git a/Mathlib/Algebra/Module/LocalizedModule/Int.lean b/Mathlib/Algebra/Module/LocalizedModule/Int.lean
@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Module.LocalizedModule.Basic
 
 /-!
-
 # Integer elements of a localized module
 
 This is a mirror of the corresponding notion for localizations of rings.

diff --git a/Mathlib/Algebra/Module/Projective.lean b/Mathlib/Algebra/Module/Projective.lean
@@ -10,7 +10,6 @@ public import Mathlib.LinearAlgebra.TensorProduct.Basis
 public import Mathlib.Logic.UnivLE
 
 /-!
-
 # Projective modules
 
 This file contains a definition of a projective module, the proof that

diff --git a/Mathlib/Algebra/Module/SnakeLemma.lean b/Mathlib/Algebra/Module/SnakeLemma.lean
@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Exact.Basic
 
 /-!
-
 # The snake lemma in terms of modules
 
 The snake lemma is proven in `Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean` for all abelian

diff --git a/Mathlib/Algebra/Module/Submodule/Defs.lean b/Mathlib/Algebra/Module/Submodule/Defs.lean
@@ -10,7 +10,6 @@ public import Mathlib.GroupTheory.GroupAction.SubMulAction
 public import Mathlib.Algebra.Group.Submonoid.Basic
 
 /-!
-
 # Submodules of a module
 
 In this file we define

diff --git a/Mathlib/Algebra/Module/Submodule/IterateMapComap.lean b/Mathlib/Algebra/Module/Submodule/IterateMapComap.lean
@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Module.Submodule.Ker
 
 /-!
-
 # Iterate maps and comaps of submodules
 
 Some preliminary work for establishing the strong rank condition for Noetherian rings.

diff --git a/Mathlib/Algebra/Module/Submodule/Lattice.lean b/Mathlib/Algebra/Module/Submodule/Lattice.lean
@@ -22,7 +22,6 @@ This file defines the lattice structure on submodules, `Submodule.CompleteLattic
 defined as `{0}` and `⊓` defined as intersection of the underlying carrier.
 If `p` and `q` are submodules of a module, `p ≤ q` means that `p ⊆ q`.
 
-
 ## Implementation notes
 
 This structure should match the `AddSubmonoid.CompleteLattice` structure, and we should try

diff --git a/Mathlib/Algebra/Module/Submodule/LinearMap.lean b/Mathlib/Algebra/Module/Submodule/LinearMap.lean
@@ -10,7 +10,6 @@ public import Mathlib.Algebra.Module.Submodule.Defs
 public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
 
 /-!
-
 # Linear maps involving submodules of a module
 
 In this file we define a number of linear maps involving submodules of a module.

diff --git a/Mathlib/Algebra/Module/Submodule/RestrictScalars.lean b/Mathlib/Algebra/Module/Submodule/RestrictScalars.lean
@@ -10,7 +10,6 @@ public import Mathlib.Algebra.Module.Submodule.Lattice
 public import Mathlib.Order.Hom.CompleteLattice
 
 /-!
-
 # Restriction of scalars for submodules
 
 If semiring `S` acts on a semiring `R` and `M` is a module over both (compatibly with this action)

diff --git a/Mathlib/Algebra/MonoidAlgebra/Degree.lean b/Mathlib/Algebra/MonoidAlgebra/Degree.lean
@@ -27,7 +27,6 @@ variable {R R' A T B ι : Type*}
 namespace AddMonoidAlgebra
 
 /-!
-
 ## sup-degree and inf-degree of an `AddMonoidAlgebra`
 
 Let `R` be a semiring and let `A` be a `SemilatticeSup`.
@@ -78,7 +77,6 @@ variable [Semiring R]
 section ExplicitDegrees
 
 /-!
-
 In this section, we use `degb` and `degt` to denote "degree functions" on `A` with values in
 a type with *b*ot or *t*op respectively.
 -/

diff --git a/Mathlib/Algebra/MvPolynomial/Monad.lean b/Mathlib/Algebra/MvPolynomial/Monad.lean
@@ -9,7 +9,6 @@ public import Mathlib.Algebra.MvPolynomial.Rename
 public import Mathlib.Algebra.MvPolynomial.Variables
 
 /-!
-
 # Monad operations on `MvPolynomial`
 
 This file defines two monadic operations on `MvPolynomial`. Given `p : MvPolynomial σ R`,

diff --git a/Mathlib/Algebra/MvPolynomial/Variables.lean b/Mathlib/Algebra/MvPolynomial/Variables.lean
@@ -16,7 +16,6 @@ This file establishes many results about the variable sets of a multivariate pol
 The *variable set* of a polynomial $P \in R[X]$ is a `Finset` containing each $x \in X$
 that appears in a monomial in $P$.
 
-
 ## Main declarations
 
 * `MvPolynomial.vars p` : the finset of variables occurring in `p`.

diff --git a/Mathlib/Algebra/Order/Antidiag/FinsuppEquiv.lean b/Mathlib/Algebra/Order/Antidiag/FinsuppEquiv.lean
@@ -11,7 +11,6 @@ public import Mathlib.Data.Finsupp.Multiset
 import Mathlib.Data.Sym.Card
 
 /-!
-
 # Equivalence between `Finset.finsuppAntidiag` and `Sym`
 
 This file collects further results about equivalence and cardinality related to

diff --git a/Mathlib/Algebra/Order/Chebyshev.lean b/Mathlib/Algebra/Order/Chebyshev.lean
@@ -19,7 +19,6 @@ This file proves the Chebyshev sum inequality.
 Chebyshev's inequality states `(∑ i ∈ s, f i) * (∑ i ∈ s, g i) ≤ #s * ∑ i ∈ s, f i * g i`
 when `f g : ι → α` monovary, and the reverse inequality when `f` and `g` antivary.
 
-
 ## Main declarations
 
 * `MonovaryOn.sum_mul_sum_le_card_mul_sum`: Chebyshev's inequality.

diff --git a/Mathlib/Algebra/Order/GroupWithZero/WithZero.lean b/Mathlib/Algebra/Order/GroupWithZero/WithZero.lean
@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Order.GroupWithZero.Basic
 public import Mathlib.Algebra.Order.GroupWithZero.Canonical
 /-!
-
 # Covariant instances on `WithZero`
 
 Adding a zero to a type with a preorder and multiplication which satisfies some

diff --git a/Mathlib/Algebra/Order/Hom/TypeTags.lean b/Mathlib/Algebra/Order/Hom/TypeTags.lean
@@ -10,7 +10,6 @@ public import Mathlib.Algebra.Order.Hom.Monoid
 public import Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
 
 /-!
-
 # Order Monoid Isomorphisms on `Additive` and `Multiplicative`.
 
 -/

diff --git a/Mathlib/Algebra/Order/Module/Defs.lean b/Mathlib/Algebra/Order/Module/Defs.lean
@@ -29,7 +29,6 @@ purposes, and the system is set up so that they imply the correct granular typec
 If those are enough for you, you may stop reading here! Else, beware that what
 follows is a bit technical.
 
-
 In all that follows, `α` and `β` are orders which have a `0` and such that `α` acts on `β` by scalar
 multiplication. Note however that we do not use lawfulness of this action in most of the file. Hence
 `•` should be considered here as a mostly arbitrary function `α → β → β`.

diff --git a/Mathlib/Algebra/Order/Module/Synonym.lean b/Mathlib/Algebra/Order/Module/Synonym.lean
@@ -12,7 +12,6 @@ public import Mathlib.Algebra.Order.Ring.Synonym
 /-!
 # Action instances for `OrderDual`
 
-
 This PR transfers group action with zero instances from a type `α` to `αᵒᵈ` and `Lex α`. Note that
 the `SMul` instances are already defined in `Mathlib/Algebra/Order/Group/Synonym.lean`.
-Original file line number
+Diff line change
@@ Expand Up / @@ -8,7 +8,6 @@ module @@
     public import Mathlib.Algebra.Algebra.Tower
     /-!
     # The `RestrictScalars` type alias
     See the documentation attached to the `RestrictScalars` definition for advice on how and when to
@@ Expand Down @@