Limit to a single blank line

Author: harahu

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.

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

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`.

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

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

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

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

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

Mathlib/Algebra/Module/FinitePresentation.lean

@@ -36,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
@@ -49,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`.
 -/

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