From 05308e6ecd525179d18d258fae90357911cd3e7b Mon Sep 17 00:00:00 2001 From: int-y1 Date: Tue, 10 Oct 2023 00:35:30 -0700 Subject: [PATCH] chore: remove trailing space in backticks --- Mathlib/Algebra/Category/AlgebraCat/Basic.lean | 2 +- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean | 4 ++-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean | 2 +- Mathlib/Algebra/Module/Basic.lean | 2 +- Mathlib/Algebra/Module/Equiv.lean | 2 +- Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean | 2 +- .../Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean | 4 ++-- Mathlib/Analysis/Convex/Jensen.lean | 2 +- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean | 2 +- Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean | 2 +- Mathlib/CategoryTheory/ConcreteCategory/Basic.lean | 2 +- Mathlib/CategoryTheory/Endomorphism.lean | 2 +- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean | 2 +- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean | 2 +- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean | 2 +- Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean | 2 +- Mathlib/CategoryTheory/Subobject/Comma.lean | 2 +- Mathlib/Combinatorics/Catalan.lean | 2 +- Mathlib/Combinatorics/SimpleGraph/Basic.lean | 2 +- Mathlib/Data/Finsupp/ToDFinsupp.lean | 2 +- Mathlib/Data/Seq/Seq.lean | 2 +- Mathlib/FieldTheory/Separable.lean | 2 +- Mathlib/Geometry/Manifold/ContMDiff.lean | 2 +- Mathlib/GroupTheory/GroupAction/Prod.lean | 2 +- Mathlib/LinearAlgebra/Basic.lean | 2 +- Mathlib/LinearAlgebra/Dimension.lean | 2 +- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 2 +- Mathlib/MeasureTheory/Function/LpSpace.lean | 2 +- Mathlib/MeasureTheory/Measure/Haar/Quotient.lean | 4 ++-- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 2 +- Mathlib/NumberTheory/NumberField/Units.lean | 2 +- Mathlib/Order/Filter/Bases.lean | 2 +- Mathlib/Order/PartialSups.lean | 2 +- Mathlib/Probability/Independence/Basic.lean | 4 ++-- Mathlib/RingTheory/Discriminant.lean | 2 +- Mathlib/RingTheory/Ideal/QuotientOperations.lean | 2 +- Mathlib/RingTheory/Prime.lean | 2 +- Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean | 2 +- Mathlib/Topology/NoetherianSpace.lean | 4 ++-- Mathlib/Topology/UniformSpace/UniformConvergence.lean | 2 +- 40 files changed, 45 insertions(+), 45 deletions(-) diff --git a/Mathlib/Algebra/Category/AlgebraCat/Basic.lean b/Mathlib/Algebra/Category/AlgebraCat/Basic.lean index 1e07bd0ba4848..318110bc366df 100644 --- a/Mathlib/Algebra/Category/AlgebraCat/Basic.lean +++ b/Mathlib/Algebra/Category/AlgebraCat/Basic.lean @@ -13,7 +13,7 @@ import Mathlib.Algebra.Category.ModuleCat.Basic /-! # Category instance for algebras over a commutative ring -We introduce the bundled category `AlgebraCat` of algebras over a fixed commutative ring `R ` along +We introduce the bundled category `AlgebraCat` of algebras over a fixed commutative ring `R` along with the forgetful functors to `RingCat` and `ModuleCat`. We furthermore show that the functor associating to a type the free `R`-algebra on that type is left adjoint to the forgetful functor. -/ diff --git a/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean index 24a6ee1a492ac..c6b79f6b447a7 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean @@ -54,11 +54,11 @@ structure LeftHomologyData where π : K ⟶ H /-- the kernel condition for `i` -/ wi : i ≫ S.g = 0 - /-- `i : K ⟶ S.X₂ ` is a kernel of `g : S.X₂ ⟶ S.X₃` -/ + /-- `i : K ⟶ S.X₂` is a kernel of `g : S.X₂ ⟶ S.X₃` -/ hi : IsLimit (KernelFork.ofι i wi) /-- the cokernel condition for `π` -/ wπ : hi.lift (KernelFork.ofι _ S.zero) ≫ π = 0 - /-- `π : K ⟶ H ` is a cokernel of the induced morphism `S.f' : S.X₁ ⟶ K` -/ + /-- `π : K ⟶ H` is a cokernel of the induced morphism `S.f' : S.X₁ ⟶ K` -/ hπ : IsColimit (CokernelCofork.ofπ π wπ) initialize_simps_projections LeftHomologyData (-hi, -hπ) diff --git a/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean index c71597dad43e1..88dfed0c3ef48 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean @@ -116,7 +116,7 @@ lemma ι_descQ_eq_zero_of_boundary (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A) (hx : k congr 1 simp only [← cancel_epi h.p, hx, p_descQ, p_g'_assoc] -/-- For `h : S.RightHomologyData`, this is a restatement of `h.hι `, saying that +/-- For `h : S.RightHomologyData`, this is a restatement of `h.hι`, saying that `ι : h.H ⟶ h.Q` is a kernel of `h.g' : h.Q ⟶ S.X₃`. -/ def hι' : IsLimit (KernelFork.ofι h.ι h.ι_g') := h.hι diff --git a/Mathlib/Algebra/Module/Basic.lean b/Mathlib/Algebra/Module/Basic.lean index 4222a2820535e..0d5a2c5736766 100644 --- a/Mathlib/Algebra/Module/Basic.lean +++ b/Mathlib/Algebra/Module/Basic.lean @@ -156,7 +156,7 @@ See note [reducible non-instances]. -/ @[reducible] def Module.compHom [Semiring S] (f : S →+* R) : Module S M := { MulActionWithZero.compHom M f.toMonoidWithZeroHom, DistribMulAction.compHom M (f : S →* R) with - -- Porting note: the `show f (r + s) • x = f r • x + f s • x ` wasn't needed in mathlib3. + -- Porting note: the `show f (r + s) • x = f r • x + f s • x` wasn't needed in mathlib3. -- Somehow, now that `SMul` is heterogeneous, it can't unfold earlier fields of a definition for -- use in later fields. See -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Heterogeneous.20scalar.20multiplication diff --git a/Mathlib/Algebra/Module/Equiv.lean b/Mathlib/Algebra/Module/Equiv.lean index 2ad31a6362328..aa0e51bf8fb0f 100644 --- a/Mathlib/Algebra/Module/Equiv.lean +++ b/Mathlib/Algebra/Module/Equiv.lean @@ -95,7 +95,7 @@ class SemilinearEquivClass (F : Type*) {R S : outParam (Type*)} [Semiring R] [Se (σ : outParam <| R →+* S) {σ' : outParam <| S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M M₂ : outParam (Type*)) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends AddEquivClass F M M₂ where - /-- Applying a semilinear equivalence `f` over `σ` to `r • x ` equals `σ r • f x`. -/ + /-- Applying a semilinear equivalence `f` over `σ` to `r • x` equals `σ r • f x`. -/ map_smulₛₗ : ∀ (f : F) (r : R) (x : M), f (r • x) = σ r • f x #align semilinear_equiv_class SemilinearEquivClass diff --git a/Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean b/Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean index 3fecdb747894a..a4bad863d0424 100644 --- a/Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean +++ b/Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean @@ -100,7 +100,7 @@ namespace MorphComponents variable {X} {n : ℕ} {Z Z' : C} (f : MorphComponents X n Z) (g : X' ⟶ X) (h : Z ⟶ Z') -/-- The morphism `X _[n+1] ⟶ Z ` associated to `f : MorphComponents X n Z`. -/ +/-- The morphism `X _[n+1] ⟶ Z` associated to `f : MorphComponents X n Z`. -/ def φ {Z : C} (f : MorphComponents X n Z) : X _[n + 1] ⟶ Z := PInfty.f (n + 1) ≫ f.a + ∑ i : Fin (n + 1), (P i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b (Fin.rev i) diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean index e45ce4f90fbd5..529673149cb43 100644 --- a/Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean +++ b/Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean @@ -38,12 +38,12 @@ theorem atImInfty_mem (S : Set ℍ) : S ∈ atImInfty ↔ ∃ A : ℝ, ∀ z : simp only [atImInfty_basis.mem_iff, true_and]; rfl #align upper_half_plane.at_im_infty_mem UpperHalfPlane.atImInfty_mem -/-- A function ` f : ℍ → α` is bounded at infinity if it is bounded along `atImInfty`. -/ +/-- A function `f : ℍ → α` is bounded at infinity if it is bounded along `atImInfty`. -/ def IsBoundedAtImInfty {α : Type*} [Norm α] (f : ℍ → α) : Prop := BoundedAtFilter atImInfty f #align upper_half_plane.is_bounded_at_im_infty UpperHalfPlane.IsBoundedAtImInfty -/-- A function ` f : ℍ → α` is zero at infinity it is zero along `atImInfty`. -/ +/-- A function `f : ℍ → α` is zero at infinity it is zero along `atImInfty`. -/ def IsZeroAtImInfty {α : Type*} [Zero α] [TopologicalSpace α] (f : ℍ → α) : Prop := ZeroAtFilter atImInfty f #align upper_half_plane.is_zero_at_im_infty UpperHalfPlane.IsZeroAtImInfty diff --git a/Mathlib/Analysis/Convex/Jensen.lean b/Mathlib/Analysis/Convex/Jensen.lean index a73d553653e06..887ee72c59d3d 100644 --- a/Mathlib/Analysis/Convex/Jensen.lean +++ b/Mathlib/Analysis/Convex/Jensen.lean @@ -23,7 +23,7 @@ Jensen's inequalities: * `ConcaveOn.le_map_centerMass`, `ConcaveOn.le_map_sum`: Concave Jensen's inequality. As corollaries, we get: -* `ConvexOn.exists_ge_of_mem_convexHull `: Maximum principle for convex functions. +* `ConvexOn.exists_ge_of_mem_convexHull`: Maximum principle for convex functions. * `ConcaveOn.exists_le_of_mem_convexHull`: Minimum principle for concave functions. -/ diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean index 91a713403acea..36131f9a888b4 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean @@ -28,7 +28,7 @@ open Finset Set namespace NNReal -/-- The nonnegative real power function `x^y`, defined for `x : ℝ≥0` and `y : ℝ ` as the +/-- The nonnegative real power function `x^y`, defined for `x : ℝ≥0` and `y : ℝ` as the restriction of the real power function. For `x > 0`, it is equal to `exp (y log x)`. For `x = 0`, one sets `0 ^ 0 = 1` and `0 ^ y = 0` for `y ≠ 0`. -/ noncomputable def rpow (x : ℝ≥0) (y : ℝ) : ℝ≥0 := diff --git a/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean b/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean index 470739a111939..6799e71dec91e 100644 --- a/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean +++ b/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean @@ -40,7 +40,7 @@ open scoped Polynomial for `x ≤ 0`. It is a basic building block to construct smooth partitions of unity. Its main property is that it vanishes for `x ≤ 0`, it is positive for `x > 0`, and the junction between the two behaviors is flat enough to retain smoothness. The fact that this function is `C^∞` is proved in -`expNegInvGlue.contDiff `. -/ +`expNegInvGlue.contDiff`. -/ def expNegInvGlue (x : ℝ) : ℝ := if x ≤ 0 then 0 else exp (-x⁻¹) #align exp_neg_inv_glue expNegInvGlue diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean index f7ad17e86ea76..a3d280b47126b 100644 --- a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean +++ b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean @@ -205,7 +205,7 @@ class HasForget₂ (C : Type u) (D : Type u') [Category.{v} C] [ConcreteCategory #align category_theory.has_forget₂ CategoryTheory.HasForget₂ /-- The forgetful functor `C ⥤ D` between concrete categories for which we have an instance -`HasForget₂ C `. -/ +`HasForget₂ C`. -/ @[reducible] def forget₂ (C : Type u) (D : Type u') [Category.{v} C] [ConcreteCategory.{w} C] [Category.{v'} D] [ConcreteCategory.{w} D] [HasForget₂ C D] : C ⥤ D := diff --git a/Mathlib/CategoryTheory/Endomorphism.lean b/Mathlib/CategoryTheory/Endomorphism.lean index ad56852a6d4ad..5e769eaa7691e 100644 --- a/Mathlib/CategoryTheory/Endomorphism.lean +++ b/Mathlib/CategoryTheory/Endomorphism.lean @@ -17,7 +17,7 @@ import Mathlib.GroupTheory.GroupAction.Defs Definition and basic properties of endomorphisms and automorphisms of an object in a category. For each `X : C`, we provide `CategoryTheory.End X := X ⟶ X` with a monoid structure, -and `CategoryTheory.Aut X := X ≅ X ` with a group structure. +and `CategoryTheory.Aut X := X ≅ X` with a group structure. -/ diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean index 7a5fe809c8be6..fb61c67233f3f 100644 --- a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean +++ b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean @@ -197,7 +197,7 @@ def preservesInitialOfIsIso (f : ⊥_ D ⟶ G.obj (⊥_ C)) [i : IsIso f] : exact PreservesInitial.ofIsoComparison G #align category_theory.limits.preserves_initial_of_is_iso CategoryTheory.Limits.preservesInitialOfIsIso -/-- If there is any isomorphism `⊥ ≅ G.obj ⊥ `, then `G` preserves initial objects. -/ +/-- If there is any isomorphism `⊥ ≅ G.obj ⊥`, then `G` preserves initial objects. -/ def preservesInitialOfIso (f : ⊥_ D ≅ G.obj (⊥_ C)) : PreservesColimit (Functor.empty C) G := preservesInitialOfIsIso G f.hom #align category_theory.limits.preserves_initial_of_iso CategoryTheory.Limits.preservesInitialOfIso diff --git a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean index 85a03d97b06ac..b746e86e5bb9b 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean @@ -532,7 +532,7 @@ abbrev prod (X Y : C) [HasBinaryProduct X Y] := limit (pair X Y) #align category_theory.limits.prod CategoryTheory.Limits.prod -/-- If we have a coproduct of `X` and `Y`, we can access it using `coprod X Y ` or +/-- If we have a coproduct of `X` and `Y`, we can access it using `coprod X Y` or `X ⨿ Y`. -/ abbrev coprod (X Y : C) [HasBinaryCoproduct X Y] := colimit (pair X Y) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean index 6f3c92d0fa761..5188a501193e7 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean @@ -1361,7 +1361,7 @@ def getBinaryBiproductData (P Q : C) [HasBinaryBiproduct P Q] : BinaryBiproductD Classical.choice HasBinaryBiproduct.exists_binary_biproduct #align category_theory.limits.get_binary_biproduct_data CategoryTheory.Limits.getBinaryBiproductData -/-- A bicone for `P Q ` which is both a limit cone and a colimit cocone. -/ +/-- A bicone for `P Q` which is both a limit cone and a colimit cocone. -/ def BinaryBiproduct.bicone (P Q : C) [HasBinaryBiproduct P Q] : BinaryBicone P Q := (getBinaryBiproductData P Q).bicone #align category_theory.limits.binary_biproduct.bicone CategoryTheory.Limits.BinaryBiproduct.bicone diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean index 4cb70aaf5401b..7b36b40597842 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean @@ -1329,7 +1329,7 @@ instance pushout.inr_of_epi {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout PushoutCocone.epi_inr_of_is_pushout_of_epi (colimit.isColimit _) #align category_theory.limits.pushout.inr_of_epi CategoryTheory.Limits.pushout.inr_of_epi -/-- The map ` X ⨿ Y ⟶ X ⨿[Z] Y` is epi. -/ +/-- The map `X ⨿ Y ⟶ X ⨿[Z] Y` is epi. -/ instance epi_coprod_to_pushout {C : Type*} [Category C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] [HasBinaryCoproduct Y Z] : Epi (coprod.desc pushout.inl pushout.inr : _ ⟶ pushout f g) := diff --git a/Mathlib/CategoryTheory/Subobject/Comma.lean b/Mathlib/CategoryTheory/Subobject/Comma.lean index 667b10889da25..5b054bda3782f 100644 --- a/Mathlib/CategoryTheory/Subobject/Comma.lean +++ b/Mathlib/CategoryTheory/Subobject/Comma.lean @@ -17,7 +17,7 @@ and `S : D` as a subtype of the subobjects of `A.right`. We deduce that `Structu well-powered if `C` is. ## Main declarations -* `StructuredArrow.subobjectEquiv `: the order-equivalence between `Subobject A` and a subtype of +* `StructuredArrow.subobjectEquiv`: the order-equivalence between `Subobject A` and a subtype of `Subobject A.right`. ## Implementation notes diff --git a/Mathlib/Combinatorics/Catalan.lean b/Mathlib/Combinatorics/Catalan.lean index 169813d9dd296..8e1ffd2835c4d 100644 --- a/Mathlib/Combinatorics/Catalan.lean +++ b/Mathlib/Combinatorics/Catalan.lean @@ -27,7 +27,7 @@ triangulations of convex polygons. ## Main results -* `catalan_eq_centralBinom_div `: The explicit formula for the Catalan number using the central +* `catalan_eq_centralBinom_div`: The explicit formula for the Catalan number using the central binomial coefficient, `catalan n = Nat.centralBinom n / (n + 1)`. * `treesOfNodesEq_card_eq_catalan`: The number of binary trees with `n` internal nodes diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean index 6a8750ecf5486..468265415b52f 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean @@ -1682,7 +1682,7 @@ abbrev Hom := #align simple_graph.hom SimpleGraph.Hom /-- A graph embedding is an embedding `f` such that for vertices `v w : V`, -`G.Adj (f v) (f w) ↔ G.Adj v w `. Its image is an induced subgraph of G'. +`G.Adj (f v) (f w) ↔ G.Adj v w`. Its image is an induced subgraph of G'. The notation `G ↪g G'` represents the type of graph embeddings. -/ abbrev Embedding := diff --git a/Mathlib/Data/Finsupp/ToDFinsupp.lean b/Mathlib/Data/Finsupp/ToDFinsupp.lean index 8eeddf626115b..644f96dbf8206 100644 --- a/Mathlib/Data/Finsupp/ToDFinsupp.lean +++ b/Mathlib/Data/Finsupp/ToDFinsupp.lean @@ -255,7 +255,7 @@ def finsuppLequivDFinsupp [DecidableEq ι] [Semiring R] [AddCommMonoid M] map_add' := Finsupp.toDFinsupp_add } #align finsupp_lequiv_dfinsupp finsuppLequivDFinsupp --- porting note: `simps` generated as ` ↑(finsuppLequivDFinsupp R).toLinearMap = Finsupp.toDFinsupp` +-- porting note: `simps` generated as `↑(finsuppLequivDFinsupp R).toLinearMap = Finsupp.toDFinsupp` @[simp] theorem finsuppLequivDFinsupp_apply_apply [DecidableEq ι] [Semiring R] [AddCommMonoid M] [∀ m : M, Decidable (m ≠ 0)] [Module R M] : diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean index 9b9cade0f229d..b85fb47702df6 100644 --- a/Mathlib/Data/Seq/Seq.lean +++ b/Mathlib/Data/Seq/Seq.lean @@ -166,7 +166,7 @@ theorem le_stable (s : Seq α) {m n} (h : m ≤ n) : s.get? m = none → s.get? exacts [id, fun h2 => al (IH h2)] #align stream.seq.le_stable Stream'.Seq.le_stable -/-- If a sequence terminated at position `n`, it also terminated at `m ≥ n `. -/ +/-- If a sequence terminated at position `n`, it also terminated at `m ≥ n`. -/ theorem terminated_stable : ∀ (s : Seq α) {m n : ℕ}, m ≤ n → s.TerminatedAt m → s.TerminatedAt n := le_stable #align stream.seq.terminated_stable Stream'.Seq.terminated_stable diff --git a/Mathlib/FieldTheory/Separable.lean b/Mathlib/FieldTheory/Separable.lean index 28ab25b6b9702..cdf49bf551dec 100644 --- a/Mathlib/FieldTheory/Separable.lean +++ b/Mathlib/FieldTheory/Separable.lean @@ -395,7 +395,7 @@ theorem unique_separable_of_irreducible {f : F[X]} (hf : Irreducible f) (hp : 0 end CharP -/-- If `n ≠ 0` in `F`, then ` X ^ n - a` is separable for any `a ≠ 0`. -/ +/-- If `n ≠ 0` in `F`, then `X ^ n - a` is separable for any `a ≠ 0`. -/ theorem separable_X_pow_sub_C {n : ℕ} (a : F) (hn : (n : F) ≠ 0) (ha : a ≠ 0) : Separable (X ^ n - C a) := separable_X_pow_sub_C_unit (Units.mk0 a ha) (IsUnit.mk0 (n : F) hn) diff --git a/Mathlib/Geometry/Manifold/ContMDiff.lean b/Mathlib/Geometry/Manifold/ContMDiff.lean index 540d1c2f2eae2..6067957dc9bb7 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff.lean @@ -16,7 +16,7 @@ basic properties of these notions. ## Main definitions and statements -Let `M ` and `M'` be two smooth manifolds, with respect to model with corners `I` and `I'`. Let +Let `M` and `M'` be two smooth manifolds, with respect to model with corners `I` and `I'`. Let `f : M → M'`. * `ContMDiffWithinAt I I' n f s x` states that the function `f` is `Cⁿ` within the set `s` diff --git a/Mathlib/GroupTheory/GroupAction/Prod.lean b/Mathlib/GroupTheory/GroupAction/Prod.lean index 940fd29bfc7c0..4bcee54a46fc5 100644 --- a/Mathlib/GroupTheory/GroupAction/Prod.lean +++ b/Mathlib/GroupTheory/GroupAction/Prod.lean @@ -13,7 +13,7 @@ import Mathlib.GroupTheory.GroupAction.Defs This file defines instances for binary product of additive and multiplicative actions and provides scalar multiplication as a homomorphism from `α × β` to `β`. ## Main declarations -* `smulMulHom `/`smulMonoidHom `: Scalar multiplication bundled as a multiplicative/monoid +* `smulMulHom`/`smulMonoidHom`: Scalar multiplication bundled as a multiplicative/monoid homomorphism. ## See also * `Mathlib.GroupTheory.GroupAction.Option` diff --git a/Mathlib/LinearAlgebra/Basic.lean b/Mathlib/LinearAlgebra/Basic.lean index f7e19f9222bbf..943af4117cecf 100644 --- a/Mathlib/LinearAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/Basic.lean @@ -1519,7 +1519,7 @@ theorem map_subtype_le (p' : Submodule R p) : map p.subtype p' ≤ p := by #align submodule.map_subtype_le Submodule.map_subtype_le /-- Under the canonical linear map from a submodule `p` to the ambient space `M`, the image of the -maximal submodule of `p` is just `p `. -/ +maximal submodule of `p` is just `p`. -/ -- @[simp] -- Porting note: simp can prove this theorem map_subtype_top : map p.subtype (⊤ : Submodule R p) = p := by simp #align submodule.map_subtype_top Submodule.map_subtype_top diff --git a/Mathlib/LinearAlgebra/Dimension.lean b/Mathlib/LinearAlgebra/Dimension.lean index ce8bb30827dba..6a9f242beee81 100644 --- a/Mathlib/LinearAlgebra/Dimension.lean +++ b/Mathlib/LinearAlgebra/Dimension.lean @@ -566,7 +566,7 @@ theorem mk_eq_mk_of_basis (v : Basis ι R M) (v' : Basis ι' R M) : #align mk_eq_mk_of_basis mk_eq_mk_of_basis /-- Given two bases indexed by `ι` and `ι'` of an `R`-module, where `R` satisfies the invariant -basis number property, an equiv `ι ≃ ι' `. -/ +basis number property, an equiv `ι ≃ ι'`. -/ def Basis.indexEquiv (v : Basis ι R M) (v' : Basis ι' R M) : ι ≃ ι' := (Cardinal.lift_mk_eq'.1 <| mk_eq_mk_of_basis v v').some #align basis.index_equiv Basis.indexEquiv diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index c592b9c18a6c8..f3adad6df039f 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -1276,7 +1276,7 @@ variable (R M M₂) /-- The space of multilinear maps on `∀ (i : Fin (n+1)), M i` is canonically isomorphic to the space of linear maps from `M 0` to the space of multilinear maps on -`∀ (i : Fin n), M i.succ `, by separating the first variable. We register this isomorphism as a +`∀ (i : Fin n), M i.succ`, by separating the first variable. We register this isomorphism as a linear isomorphism in `multilinearCurryLeftEquiv R M M₂`. The direct and inverse maps are given by `f.uncurryLeft` and `f.curryLeft`. Use these diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean index 8dd8c1fb29fba..0350629d77357 100644 --- a/Mathlib/MeasureTheory/Function/LpSpace.lean +++ b/Mathlib/MeasureTheory/Function/LpSpace.lean @@ -1082,7 +1082,7 @@ namespace ContinuousLinearMap variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] -/-- Composing `f : Lp ` with `L : E →L[𝕜] F`. -/ +/-- Composing `f : Lp` with `L : E →L[𝕜] F`. -/ def compLp (L : E →L[𝕜] F) (f : Lp E p μ) : Lp F p μ := L.lipschitz.compLp (map_zero L) f #align continuous_linear_map.comp_Lp ContinuousLinearMap.compLp diff --git a/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean b/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean index ee75402c8cebe..a7654d572c760 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean @@ -17,12 +17,12 @@ subgroup of a group `G` on `G` itself. ## Main results -* `MeasureTheory.IsFundamentalDomain.smulInvariantMeasure_map `: given a subgroup `Γ` of a +* `MeasureTheory.IsFundamentalDomain.smulInvariantMeasure_map`: given a subgroup `Γ` of a topological group `G`, the pushforward to the coset space `G ⧸ Γ` of the restriction of a both left- and right-invariant measure on `G` to a fundamental domain `𝓕` is a `G`-invariant measure on `G ⧸ Γ`. -* `MeasureTheory.IsFundamentalDomain.isMulLeftInvariant_map `: given a normal subgroup `Γ` of +* `MeasureTheory.IsFundamentalDomain.isMulLeftInvariant_map`: given a normal subgroup `Γ` of a topological group `G`, the pushforward to the quotient group `G ⧸ Γ` of the restriction of a both left- and right-invariant measure on `G` to a fundamental domain `𝓕` is a left-invariant measure on `G ⧸ Γ`. diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index 785a5fef31b71..dfbad84e0bf80 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean @@ -171,7 +171,7 @@ theorem subsingleton_iff [Subsingleton B] : IsCyclotomicExtension S A B ↔ S = #align is_cyclotomic_extension.subsingleton_iff IsCyclotomicExtension.subsingleton_iff /-- If `B` is a cyclotomic extension of `A` given by roots of unity of order in `S ∪ T`, then `B` -is a cyclotomic extension of `adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 } ` given by +is a cyclotomic extension of `adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 }` given by roots of unity of order in `T`. -/ theorem union_right [h : IsCyclotomicExtension (S ∪ T) A B] : IsCyclotomicExtension T (adjoin A {b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1}) B := by diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index 7b45bb84cf7d6..2765fc6bf4a5a 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -181,7 +181,7 @@ distinguished (arbitrary) infinite place, prove that its kernel is the torsion s follows that `unitLattice` is a free `ℤ`-module (see `unitLattice_moduleFree `) of rank `card (InfinitePlaces K) - 1` (see `unitLattice_rank`). To prove that the `unitLattice` is a full `ℤ`-lattice, we need to prove that it is discrete (see `unitLattice_inter_ball_finite`) and that it -spans the full space over `ℝ` (see ` unitLattice_span_eq_top`); this is the main part of the proof, +spans the full space over `ℝ` (see `unitLattice_span_eq_top`); this is the main part of the proof, see the section `span_top` below for more details. -/ diff --git a/Mathlib/Order/Filter/Bases.lean b/Mathlib/Order/Filter/Bases.lean index e1fe100d2f0d1..819ff155ef839 100644 --- a/Mathlib/Order/Filter/Bases.lean +++ b/Mathlib/Order/Filter/Bases.lean @@ -59,7 +59,7 @@ and consequences are derived. * `isCountablyGenerated_iff_exists_antitone_basis` : proves a filter is countably generated if and only if it admits a basis parametrized by a decreasing sequence of sets indexed by `ℕ`. -* `tendsto_iff_seq_tendsto ` : an abstract version of "sequentially continuous implies continuous". +* `tendsto_iff_seq_tendsto` : an abstract version of "sequentially continuous implies continuous". ## Implementation notes diff --git a/Mathlib/Order/PartialSups.lean b/Mathlib/Order/PartialSups.lean index 42f639e2b2d48..3a537e7546be8 100644 --- a/Mathlib/Order/PartialSups.lean +++ b/Mathlib/Order/PartialSups.lean @@ -13,7 +13,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Finset # The monotone sequence of partial supremums of a sequence We define `partialSups : (ℕ → α) → ℕ →o α` inductively. For `f : ℕ → α`, `partialSups f` is -the sequence `f 0 `, `f 0 ⊔ f 1`, `f 0 ⊔ f 1 ⊔ f 2`, ... The point of this definition is that +the sequence `f 0`, `f 0 ⊔ f 1`, `f 0 ⊔ f 1 ⊔ f 2`, ... The point of this definition is that * it doesn't need a `⨆`, as opposed to `⨆ (i ≤ n), f i` (which also means the wrong thing on `ConditionallyCompleteLattice`s). * it doesn't need a `⊥`, as opposed to `(Finset.range (n + 1)).sup f`. diff --git a/Mathlib/Probability/Independence/Basic.lean b/Mathlib/Probability/Independence/Basic.lean index 671abecd96c1b..976ae8945b3b6 100644 --- a/Mathlib/Probability/Independence/Basic.lean +++ b/Mathlib/Probability/Independence/Basic.lean @@ -12,7 +12,7 @@ import Mathlib.Probability.Independence.Kernel * A family of sets of sets `π : ι → Set (Set Ω)` is independent with respect to a measure `μ` if for any finite set of indices `s = {i_1, ..., i_n}`, for any sets `f i_1 ∈ π i_1, ..., f i_n ∈ π i_n`, - `μ (⋂ i in s, f i) = ∏ i in s, μ (f i) `. It will be used for families of π-systems. + `μ (⋂ i in s, f i) = ∏ i in s, μ (f i)`. It will be used for families of π-systems. * A family of measurable space structures (i.e. of σ-algebras) is independent with respect to a measure `μ` (typically defined on a finer σ-algebra) if the family of sets of measurable sets they define is independent. I.e., `m : ι → MeasurableSpace Ω` is independent with respect to a @@ -97,7 +97,7 @@ def IndepSets [MeasurableSpace Ω] (s1 s2 : Set (Set Ω)) (μ : Measure Ω := by measure `μ` (typically defined on a finer σ-algebra) if the family of sets of measurable sets they define is independent. `m : ι → MeasurableSpace Ω` is independent with respect to measure `μ` if for any finite set of indices `s = {i_1, ..., i_n}`, for any sets -`f i_1 ∈ m i_1, ..., f i_n ∈ m i_n`, then `μ (⋂ i in s, f i) = ∏ i in s, μ (f i) `. -/ +`f i_1 ∈ m i_1, ..., f i_n ∈ m i_n`, then `μ (⋂ i in s, f i) = ∏ i in s, μ (f i)`. -/ def iIndep (m : ι → MeasurableSpace Ω) [MeasurableSpace Ω] (μ : Measure Ω := by volume_tac) : Prop := kernel.iIndep m (kernel.const Unit μ) (Measure.dirac () : Measure Unit) diff --git a/Mathlib/RingTheory/Discriminant.lean b/Mathlib/RingTheory/Discriminant.lean index 8b97f16c6350a..5ba6c01f0ecc1 100644 --- a/Mathlib/RingTheory/Discriminant.lean +++ b/Mathlib/RingTheory/Discriminant.lean @@ -35,7 +35,7 @@ Given an `A`-algebra `B` and `b`, an `ι`-indexed family of elements of `B`, we field `E` corresponding to `j : ι` via a bijection `e : ι ≃ (L →ₐ[K] E)`. * `Algebra.discr_powerBasis_eq_prod` : the discriminant of a power basis. * `Algebra.discr_isIntegral` : if `K` and `L` are fields and `IsScalarTower R K L`, if - `b : ι → L` satisfies ` ∀ i, IsIntegral R (b i)`, then `IsIntegral R (discr K b)`. + `b : ι → L` satisfies `∀ i, IsIntegral R (b i)`, then `IsIntegral R (discr K b)`. * `Algebra.discr_mul_isIntegral_mem_adjoin` : let `K` be the fraction field of an integrally closed domain `R` and let `L` be a finite separable extension of `K`. Let `B : PowerBasis K L` be such that `IsIntegral R B.gen`. Then for all, `z : L` we have diff --git a/Mathlib/RingTheory/Ideal/QuotientOperations.lean b/Mathlib/RingTheory/Ideal/QuotientOperations.lean index 201fa8c3b323f..e00895706ff03 100644 --- a/Mathlib/RingTheory/Ideal/QuotientOperations.lean +++ b/Mathlib/RingTheory/Ideal/QuotientOperations.lean @@ -682,7 +682,7 @@ theorem quotQuotEquivQuotSup_symm_quotQuotMk (x : R) : rfl #align double_quot.quot_quot_equiv_quot_sup_symm_quot_quot_mk DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk -/-- The obvious isomorphism `(R/I)/J' → (R/J)/I' ` -/ +/-- The obvious isomorphism `(R/I)/J' → (R/J)/I'` -/ def quotQuotEquivComm : (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) ≃+* (R ⧸ J) ⧸ I.map (Ideal.Quotient.mk J) := ((quotQuotEquivQuotSup I J).trans (quotEquivOfEq (sup_comm))).trans diff --git a/Mathlib/RingTheory/Prime.lean b/Mathlib/RingTheory/Prime.lean index 30dd94a9b2f58..9339c0beae414 100644 --- a/Mathlib/RingTheory/Prime.lean +++ b/Mathlib/RingTheory/Prime.lean @@ -47,7 +47,7 @@ theorem mul_eq_mul_prime_prod {α : Type*} [DecidableEq α] {x y a : R} {s : Fin simp [← hbc, prod_insert hiu, mul_assoc, mul_comm, mul_left_comm]⟩ #align mul_eq_mul_prime_prod mul_eq_mul_prime_prod -/-- If ` x * y = a * p ^ n` where `p` is prime, then `x` and `y` can both be written +/-- If `x * y = a * p ^ n` where `p` is prime, then `x` and `y` can both be written as the product of a power of `p` and a divisor of `a`. -/ theorem mul_eq_mul_prime_pow {x y a p : R} {n : ℕ} (hp : Prime p) (hx : x * y = a * p ^ n) : ∃ (i j : ℕ) (b c : R), i + j = n ∧ a = b * c ∧ x = b * p ^ i ∧ y = c * p ^ j := by diff --git a/Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean b/Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean index 984977b3e2a61..51489dbd4cf9a 100644 --- a/Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean +++ b/Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean @@ -351,7 +351,7 @@ theorem nonarchimedean (hB : SubmodulesBasis B) : @NonarchimedeanAddGroup M _ hB library_note "nonarchimedean non instances"/-- The non archimedean subgroup basis lemmas cannot be instances because some instances -(such as `MeasureTheory.AEEqFun.instAddMonoid ` or `topological_add_group.to_has_continuous_add`) +(such as `MeasureTheory.AEEqFun.instAddMonoid` or `topological_add_group.to_has_continuous_add`) cause the search for `@TopologicalAddGroup β ?m1 ?m2`, i.e. a search for a topological group where the topology/group structure are unknown. -/ diff --git a/Mathlib/Topology/NoetherianSpace.lean b/Mathlib/Topology/NoetherianSpace.lean index c6bf23a1b0c22..a4992ad97d3be 100644 --- a/Mathlib/Topology/NoetherianSpace.lean +++ b/Mathlib/Topology/NoetherianSpace.lean @@ -33,9 +33,9 @@ of a noetherian scheme (e.g., the spectrum of a noetherian ring) is noetherian. is noetherian. - `TopologicalSpace.NoetherianSpace.iUnion`: The finite union of noetherian spaces is noetherian. - `TopologicalSpace.NoetherianSpace.discrete`: A noetherian and Hausdorff space is discrete. -- `TopologicalSpace.NoetherianSpace.exists_finset_irreducible` : Every closed subset of a noetherian +- `TopologicalSpace.NoetherianSpace.exists_finset_irreducible`: Every closed subset of a noetherian space is a finite union of irreducible closed subsets. -- `TopologicalSpace.NoetherianSpace.finite_irreducibleComponents `: The number of irreducible +- `TopologicalSpace.NoetherianSpace.finite_irreducibleComponents`: The number of irreducible components of a noetherian space is finite. -/ diff --git a/Mathlib/Topology/UniformSpace/UniformConvergence.lean b/Mathlib/Topology/UniformSpace/UniformConvergence.lean index 67fdd99294a76..0bd3958d56101 100644 --- a/Mathlib/Topology/UniformSpace/UniformConvergence.lean +++ b/Mathlib/Topology/UniformSpace/UniformConvergence.lean @@ -916,7 +916,7 @@ this paragraph, we prove variations around this statement. /-- If `Fₙ` converges locally uniformly on a neighborhood of `x` within a set `s` to a function `f` -which is continuous at `x` within `s `, and `gₙ` tends to `x` within `s`, then `Fₙ (gₙ)` tends +which is continuous at `x` within `s`, and `gₙ` tends to `x` within `s`, then `Fₙ (gₙ)` tends to `f x`. -/ theorem tendsto_comp_of_locally_uniform_limit_within (h : ContinuousWithinAt f s x) (hg : Tendsto g p (𝓝[s] x))