Trim leading blank lines

# Conflicts:
#	Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean
#	Mathlib/Data/Finite/Card.lean

Author: harahu

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

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

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,

Mathlib/Algebra/Category/ContinuousCohomology/Basic.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

Mathlib/Algebra/Category/Grp/EnoughInjectives.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.

Mathlib/Algebra/Category/Grp/FiniteGrp.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,

Mathlib/Algebra/Category/ModuleCat/AB.lean

@@ -13,7 +13,6 @@ public import Mathlib.Data.Rat.Floor
 public import Mathlib.Tactic.Continuity
 
 /-!
-
 # Dimension Shifting
 
 -/

Mathlib/Algebra/Category/ModuleCat/Ext/DimensionShifting.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
 
 -/

Mathlib/Algebra/Category/ModuleCat/Ext/Finite.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