Skip to content

Commit 0bc891b

Browse files
jcommelinjcommelin
committed
chore(*): remove empty lines between variable statements
1 parent 14b7f74 commit 0bc891b

898 files changed

Lines changed: 0 additions & 3007 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Archive/Hairer.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,6 @@ variable {ι : Type*} [Fintype ι]
3232
section normed
3333
variable {𝕜 E F : Type*} [NontriviallyNormedField 𝕜]
3434
variable [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
35-
3635
variable (𝕜 E F) in
3736
/-- The set of smooth functions supported in a set `s`, as a submodule of the space of functions. -/
3837
def SmoothSupportedOn (n : ℕ∞) (s : Set E) : Submodule 𝕜 (E → F) where

‎Archive/Imo/Imo1975Q1.lean‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,7 @@ open scoped BigOperators
3030
/- Let `n` be a natural number, `x` and `y` be as in the problem statement and `σ` be the
3131
permutation of natural numbers such that `z = y ∘ σ` -/
3232
variable (n : ℕ) (σ : Equiv.Perm ℕ) (hσ : {x | σ x ≠ x} ⊆ Finset.Icc 1 n) (x y : ℕ → ℝ)
33-
3433
variable (hx : AntitoneOn x (Finset.Icc 1 n))
35-
3634
variable (hy : AntitoneOn y (Finset.Icc 1 n))
3735

3836
theorem imo1975_q1 :

‎Archive/Imo/Imo2019Q2.lean‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -68,9 +68,7 @@ set_option linter.uppercaseLean3 false
6868
attribute [local instance] FiniteDimensional.of_fact_finrank_eq_two
6969

7070
variable (V : Type*) (Pt : Type*)
71-
7271
variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]
73-
7472
variable [NormedAddTorsor V Pt] [hd2 : Fact (finrank ℝ V = 2)]
7573

7674
namespace Imo2019Q2

‎Archive/Wiedijk100Theorems/SolutionOfCubic.lean‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -44,11 +44,8 @@ section Field
4444
open Polynomial
4545

4646
variable {K : Type*} [Field K]
47-
4847
variable [Invertible (2 : K)] [Invertible (3 : K)]
49-
5048
variable (a b c d : K)
51-
5249
variable {ω p q r s t : K}
5350

5451
theorem cube_root_of_unity_sum (hω : IsPrimitiveRoot ω 3) : 1 + ω + ω ^ 2 = 0 := by

‎Mathlib/Algebra/Algebra/Basic.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -585,7 +585,6 @@ end CommSemiring
585585
section Ring
586586

587587
variable [CommRing R]
588-
589588
variable (R)
590589

591590
/-- A `Semiring` that is an `Algebra` over a commutative ring carries a natural `Ring` structure.

‎Mathlib/Algebra/Algebra/Bilinear.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -153,7 +153,6 @@ end NonUnital
153153
section Semiring
154154

155155
variable (R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
156-
157156
variable {R A B} in
158157
/-- A `LinearMap` preserves multiplication if pre- and post- composition with `LinearMap.mul` are
159158
equivalent. By converting the statement into an equality of `LinearMap`s, this lemma allows various

‎Mathlib/Algebra/Algebra/Equiv.lean‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -89,10 +89,8 @@ section Semiring
8989

9090
variable [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃]
9191
variable [Semiring A₁'] [Semiring A₂'] [Semiring A₃']
92-
9392
variable [Algebra R A₁] [Algebra R A₂] [Algebra R A₃]
9493
variable [Algebra R A₁'] [Algebra R A₂'] [Algebra R A₃']
95-
9694
variable (e : A₁ ≃ₐ[R] A₂)
9795

9896
instance : EquivLike (A₁ ≃ₐ[R] A₂) A₁ A₂ where
@@ -818,7 +816,6 @@ end Semiring
818816
section CommSemiring
819817

820818
variable [CommSemiring R] [CommSemiring A₁] [CommSemiring A₂]
821-
822819
variable [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂)
823820

824821
-- Porting note: Added nonrec
@@ -838,7 +835,6 @@ end CommSemiring
838835
section Ring
839836

840837
variable [CommSemiring R] [Ring A₁] [Ring A₂]
841-
842838
variable [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂)
843839

844840
protected theorem map_neg (x) : e (-x) = -e x :=

‎Mathlib/Algebra/Algebra/Hom.lean‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,6 @@ variable {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} {D : Type v₁}
9191
section Semiring
9292

9393
variable [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Semiring D]
94-
9594
variable [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D]
9695

9796
-- Porting note: we don't port specialized `CoeFun` instances if there is `DFunLike` instead
@@ -452,7 +451,6 @@ end Semiring
452451
section CommSemiring
453452

454453
variable [CommSemiring R] [CommSemiring A] [CommSemiring B]
455-
456454
variable [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B)
457455

458456
protected theorem map_multiset_prod (s : Multiset A) : φ s.prod = (s.map φ).prod :=
@@ -474,7 +472,6 @@ end CommSemiring
474472
section Ring
475473

476474
variable [CommSemiring R] [Ring A] [Ring B]
477-
478475
variable [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B)
479476

480477
protected theorem map_neg (x) : φ (-x) = -φ x :=
@@ -548,7 +545,6 @@ end
548545
namespace Algebra
549546

550547
variable (R : Type u) (A : Type v)
551-
552548
variable [CommSemiring R] [Semiring A] [Algebra R A]
553549

554550
/-- `AlgebraMap` as an `AlgHom`. -/
@@ -589,7 +585,6 @@ end Algebra
589585
namespace MulSemiringAction
590586

591587
variable {M G : Type*} (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A]
592-
593588
variable [Monoid M] [MulSemiringAction M A] [SMulCommClass M R A]
594589

595590
/-- Each element of the monoid defines an algebra homomorphism.

‎Mathlib/Algebra/Algebra/NonUnitalHom.lean‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -114,11 +114,8 @@ end NonUnitalAlgHomClass
114114
namespace NonUnitalAlgHom
115115

116116
variable {R A B C} [Monoid R]
117-
118117
variable [NonUnitalNonAssocSemiring A] [DistribMulAction R A]
119-
120118
variable [NonUnitalNonAssocSemiring B] [DistribMulAction R B]
121-
122119
variable [NonUnitalNonAssocSemiring C] [DistribMulAction R C]
123120

124121
-- Porting note: Replaced with DFunLike instance

‎Mathlib/Algebra/Algebra/Operations.lean‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -70,13 +70,11 @@ end SubMulAction
7070
namespace Submodule
7171

7272
variable {ι : Sort uι}
73-
7473
variable {R : Type u} [CommSemiring R]
7574

7675
section Ring
7776

7877
variable {A : Type v} [Semiring A] [Algebra R A]
79-
8078
variable (S T : Set A) {M N P Q : Submodule R A} {m n : A}
8179

8280
/-- `1 : Submodule R A` is the submodule R of A. -/
@@ -204,7 +202,6 @@ theorem span_mul_span : span R S * span R T = span R (S * T) :=
204202
#align submodule.span_mul_span Submodule.span_mul_span
205203

206204
variable {R}
207-
208205
variable (M N P Q)
209206

210207
@[simp]
@@ -625,7 +622,6 @@ end Ring
625622
section CommRing
626623

627624
variable {A : Type v} [CommSemiring A] [Algebra R A]
628-
629625
variable {M N : Submodule R A} {m n : A}
630626

631627
theorem mul_mem_mul_rev (hm : m ∈ M) (hn : n ∈ N) : n * m ∈ M * N :=

0 commit comments

Comments
 (0)