diff --git a/Mathlib/Algebra/Category/Grp/AB.lean b/Mathlib/Algebra/Category/Grp/AB.lean index 5e21a0c9355d5e..e02f411b56b441 100644 --- a/Mathlib/Algebra/Category/Grp/AB.lean +++ b/Mathlib/Algebra/Category/Grp/AB.lean @@ -15,7 +15,7 @@ public import Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono # AB axioms for the category of abelian groups This file proves that the category of abelian groups satisfies Grothendieck's axioms AB5, AB4, and -AB4*. +AB4\*. -/ @[expose] public section diff --git a/Mathlib/Algebra/Category/ModuleCat/AB.lean b/Mathlib/Algebra/Category/ModuleCat/AB.lean index ccff92713f56e8..6b104004fb17af 100644 --- a/Mathlib/Algebra/Category/ModuleCat/AB.lean +++ b/Mathlib/Algebra/Category/ModuleCat/AB.lean @@ -14,7 +14,7 @@ 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, -and AB4*. Further, it proves that `R` is a separator in the category of modules over `R`, and +and AB4\*. Further, it proves that `R` is a separator in the category of modules over `R`, and concludes that this category is Grothendieck abelian. -/ diff --git a/Mathlib/Algebra/DualNumber.lean b/Mathlib/Algebra/DualNumber.lean index 0aa6f91306f180..089fa54f44f296 100644 --- a/Mathlib/Algebra/DualNumber.lean +++ b/Mathlib/Algebra/DualNumber.lean @@ -223,7 +223,7 @@ theorem range_lift AlgHom.map_adjoin, ← AlgHom.range_comp, Set.image_singleton, lift_apply_eps, lift_comp_inlHom, Algebra.map_top] -/-- Show DualNumber with values x and y as an "x + y*ε" string -/ +/-- Show DualNumber with values x and y as an `"x + y*ε"` string -/ instance instRepr [Repr R] : Repr (DualNumber R) where reprPrec f p := (if p > 65 then (Std.Format.bracket "(" · ")") else (·)) <| diff --git a/Mathlib/Algebra/FiniteSupport/Basic.lean b/Mathlib/Algebra/FiniteSupport/Basic.lean index 681e93a977e0c4..36d1992c662788 100644 --- a/Mathlib/Algebra/FiniteSupport/Basic.lean +++ b/Mathlib/Algebra/FiniteSupport/Basic.lean @@ -13,7 +13,7 @@ public import Mathlib.Data.Set.Finite.Lattice import Mathlib.Algebra.Group.Support /-! -# Make fun_prop work for finite (multiplicative) support +# Make `fun_prop` work for finite (multiplicative) support We provide API lemmas for the predicate `HasFiniteMulSupport` (and its additivized version `HasFiniteSupport`) on functions so that `fun_prop` can prove it for functions that are diff --git a/Mathlib/Algebra/FiniteSupport/Defs.lean b/Mathlib/Algebra/FiniteSupport/Defs.lean index 45f4c9bd1d54f2..0486154c77cdf3 100644 --- a/Mathlib/Algebra/FiniteSupport/Defs.lean +++ b/Mathlib/Algebra/FiniteSupport/Defs.lean @@ -9,12 +9,12 @@ public import Mathlib.Algebra.Notation.Support public import Mathlib.Data.Set.Finite.Basic /-! -# Make fun_prop work for finite (multiplicative) support +# Make `fun_prop` work for finite (multiplicative) support We define a new predicate `HasFiniteMulSupport` (and its additivized version) on functions and provide the infrastructure so that `fun_prop` can prove it for functions that are built from other functions with finite multiplicative support. The relevant API lemmas -are provided in [Mathlib.Algebra.FiniteSupport.Basic}(Mathlib/Algebra/FiniteSupport/Basic.lean). +are provided in [Mathlib.Algebra.FiniteSupport.Basic](Mathlib/Algebra/FiniteSupport/Basic.lean). -/ @[expose] public section diff --git a/Mathlib/Algebra/Group/UniqueProds/Basic.lean b/Mathlib/Algebra/Group/UniqueProds/Basic.lean index 7ca8f897c7837f..99dceba3a82621 100644 --- a/Mathlib/Algebra/Group/UniqueProds/Basic.lean +++ b/Mathlib/Algebra/Group/UniqueProds/Basic.lean @@ -359,7 +359,7 @@ open MulOpposite in contains a unique pair with the `UniqueMul` property. Strojnowski showed that if `G` is a group, then we only need to check this when `A = B`. Here we generalize the result to cancellative semigroups. - Non-cancellative counterexample: the AddMonoid {0,1} with 1+1=1. -/ + Non-cancellative counterexample: the AddMonoid `{0,1}` with 1+1=1. -/ @[to_additive] theorem of_same {G} [Semigroup G] [IsCancelMul G] (h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2) : UniqueProds G where diff --git a/Mathlib/Algebra/Lie/DirectSum.lean b/Mathlib/Algebra/Lie/DirectSum.lean index fb08804d13fc9f..890b08ca949466 100644 --- a/Mathlib/Algebra/Lie/DirectSum.lean +++ b/Mathlib/Algebra/Lie/DirectSum.lean @@ -217,8 +217,7 @@ section Ideals variable {L : Type w} [LieRing L] [LieAlgebra R L] (I : ι → LieIdeal R L) /-- The fact that this instance is necessary seems to be a bug in typeclass inference. See -[this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ -Typeclass.20resolution.20under.20binders/near/245151099). -/ +[this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclass.20resolution.20under.20binders/near/245151099). -/ instance lieRingOfIdeals : LieRing (⨁ i, I i) := DirectSum.lieRing fun i => ↥(I i) diff --git a/Mathlib/Algebra/MonoidAlgebra/MapDomain.lean b/Mathlib/Algebra/MonoidAlgebra/MapDomain.lean index b827a88445f90b..5134fe0965918b 100644 --- a/Mathlib/Algebra/MonoidAlgebra/MapDomain.lean +++ b/Mathlib/Algebra/MonoidAlgebra/MapDomain.lean @@ -120,8 +120,8 @@ lemma comapDomain_add (f : M → N) (hf) (x y : R[N]) : lemma comapDomain_single_of_not_mem_range {r : R} {n : N} (hn : n ∉ Set.range f) (hf) : comapDomain f hf (single n r) = 0 := by simp [comapDomain, coeff, single, *] -/-- `comapDomain` as an `AddMonoidHom. -/ -@[to_additive (attr := simps) comapDomainAddMonoidHom /-- `comapDomain` as an `AddMonoidHom. -/] +/-- `comapDomain` as an `AddMonoidHom`. -/ +@[to_additive (attr := simps) comapDomainAddMonoidHom /-- `comapDomain` as an `AddMonoidHom`. -/] def comapDomainAddMonoidHom (f : M → N) (hf : Injective f) : R[N] →+ R[M] where toFun := comapDomain f hf map_zero' := by simp diff --git a/Mathlib/Algebra/Order/AddGroupWithTop.lean b/Mathlib/Algebra/Order/AddGroupWithTop.lean index 7293b887df7eb2..1f3df69de6c9bc 100644 --- a/Mathlib/Algebra/Order/AddGroupWithTop.lean +++ b/Mathlib/Algebra/Order/AddGroupWithTop.lean @@ -20,7 +20,7 @@ that show up as the target of so-called “valuations” in algebraic number the Usually, in the informal literature, these objects are constructed by taking a linearly ordered commutative additive group Γ and formally adjoining a -top element: Γ ∪ {⊤}. +top element: `Γ ∪ {⊤}`. The disadvantage is that a type such as `ENNReal` is not of that form, whereas it is a very common target for valuations. diff --git a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean index 0800da87c9f48e..004a7b9eea28a4 100644 --- a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean +++ b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean @@ -25,7 +25,7 @@ This file sets up a special class of linearly ordered commutative monoids that show up as the target of so-called “valuations” in algebraic number theory. Usually, in the informal literature, these objects are constructed -by taking a linearly ordered commutative group Γ and formally adjoining a zero element: Γ ∪ {0}. +by taking a linearly ordered commutative group Γ and formally adjoining a zero element: `Γ ∪ {0}`. The disadvantage is that a type such as `NNReal` is not of that form, whereas it is a very common target for valuations. diff --git a/Mathlib/Algebra/Order/Star/Basic.lean b/Mathlib/Algebra/Order/Star/Basic.lean index 89292e341941cc..1d2f9759964375 100644 --- a/Mathlib/Algebra/Order/Star/Basic.lean +++ b/Mathlib/Algebra/Order/Star/Basic.lean @@ -71,7 +71,7 @@ lemma smul_mem_closure_star_mul {r : R} end prereq -/-- An ordered `*`-ring is a `*`-ring with a partial order such that the nonnegative elements +/-- An ordered \*-ring is a \*-ring with a partial order such that the nonnegative elements constitute precisely the `AddSubmonoid` generated by elements of the form `star s * s`. If you are working with a `NonUnitalRing` and not a `NonUnitalSemiring`, it may be more diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean index ee96ed29f67376..45ac70fdc75648 100644 --- a/Mathlib/Algebra/Quaternion.lean +++ b/Mathlib/Algebra/Quaternion.lean @@ -1253,7 +1253,7 @@ theorem mk_univ_quaternionAlgebra : #(Set.univ : Set ℍ[R,c₁,c₂,c₃]) = #R theorem mk_univ_quaternionAlgebra_of_infinite [Infinite R] : #(Set.univ : Set ℍ[R,c₁,c₂,c₃]) = #R := by rw [mk_univ_quaternionAlgebra, pow_four] -/-- Show the quaternion ⟨w, x, y, z⟩ as a string "{ re := w, imI := x, imJ := y, imK := z }". +/-- Show the quaternion `⟨w, x, y, z⟩` as a string `"{ re := w, imI := x, imJ := y, imK := z }"`. For the typical case of quaternions over ℝ, each component will show as a Cauchy sequence due to the way Real numbers are represented. diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean index 0aa3f047f5efd3..d27cffae63f8f0 100644 --- a/Mathlib/Algebra/Star/Basic.lean +++ b/Mathlib/Algebra/Star/Basic.lean @@ -115,7 +115,7 @@ export TrivialStar (star_trivial) attribute [simp] star_trivial -/-- A `*`-magma is a magma `R` with an involutive operation `star` +/-- A \*-magma is a magma `R` with an involutive operation `star` such that `star (r * s) = star s * star r`. -/ class StarMul (R : Type u) [Mul R] extends InvolutiveStar R where @@ -202,7 +202,7 @@ theorem star_zpow [Group R] [StarMul R] (x : R) (z : ℤ) : star (x ^ z) = star theorem star_div [CommGroup R] [StarMul R] (x y : R) : star (x / y) = star x / star y := map_div (starMulAut : R ≃* R) _ _ -/-- Any commutative monoid admits the trivial `*`-structure. +/-- Any commutative monoid admits the trivial \*-structure. See note [reducible non-instances]. -/ @@ -221,7 +221,7 @@ theorem star_id_of_comm {R : Type*} [CommMonoid R] {x : R} : star x = x := end -/-- A `*`-additive monoid `R` is an additive monoid with an involutive `star` operation which +/-- A \*-additive monoid `R` is an additive monoid with an involutive `star` operation which preserves addition. -/ class StarAddMonoid (R : Type u) [AddMonoid R] extends InvolutiveStar R where /-- `star` commutes with addition -/ @@ -269,8 +269,8 @@ theorem star_nsmul [AddMonoid R] [StarAddMonoid R] (n : ℕ) (x : R) : star (n theorem star_zsmul [AddGroup R] [StarAddMonoid R] (n : ℤ) (x : R) : star (n • x) = n • star x := (starAddEquiv : R ≃+ R).toAddMonoidHom.map_zsmul _ _ -/-- A `*`-ring `R` is a non-unital, non-associative (semi)ring with an involutive `star` operation -which is additive which makes `R` with its multiplicative structure into a `*`-multiplication +/-- A \*-ring `R` is a non-unital, non-associative (semi)ring with an involutive `star` operation +which is additive which makes `R` with its multiplicative structure into a \*-multiplication (i.e. `star (r * s) = star s * star r`). -/ class StarRing (R : Type u) [NonUnitalNonAssocSemiring R] extends StarMul R where /-- `star` commutes with addition -/ @@ -370,7 +370,7 @@ theorem star_div₀ [CommGroupWithZero R] [StarMul R] (x y : R) : star (x / y) = apply op_injective rw [division_def, op_div, mul_comm, star_mul, star_inv₀, op_mul, op_inv] -/-- Any commutative semiring admits the trivial `*`-structure. +/-- Any commutative semiring admits the trivial \*-structure. See note [reducible non-instances]. -/ diff --git a/Mathlib/Algebra/Star/CHSH.lean b/Mathlib/Algebra/Star/CHSH.lean index f3805d1eb427ba..9e0fce4388a8bc 100644 --- a/Mathlib/Algebra/Star/CHSH.lean +++ b/Mathlib/Algebra/Star/CHSH.lean @@ -19,12 +19,12 @@ This is a foundational result which implies that quantum mechanics is not a local hidden variable theory. As usually stated the CHSH inequality requires substantial language from physics and probability, -but it is possible to give a statement that is purely about ordered `*`-algebras. +but it is possible to give a statement that is purely about ordered \*-algebras. We do that here, to avoid as many practical and logical dependencies as possible. -Since the algebra of observables of any quantum system is an ordered `*`-algebra +Since the algebra of observables of any quantum system is an ordered \*-algebra (in particular a von Neumann algebra) this is a strict generalization of the usual statement. -Let `R` be a `*`-ring. +Let `R` be a \*-ring. A CHSH tuple in `R` consists of * four elements `A₀ A₁ B₀ B₁ : R`, such that @@ -35,12 +35,12 @@ The physical interpretation is that the four elements are observables (hence sel that take values ±1 (hence involutions), and that the `Aᵢ` are spacelike separated from the `Bⱼ` (and hence commute). -The CHSH inequality says that when `R` is an ordered `*`-ring -(that is, a `*`-ring which is ordered, and for every `r : R`, `0 ≤ star r * r`), +The CHSH inequality says that when `R` is an ordered \*-ring +(that is, a \*-ring which is ordered, and for every `r : R`, `0 ≤ star r * r`), which is moreover *commutative*, we have `A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2` -On the other hand, Tsirelson's inequality says that for any ordered `*`-ring we have +On the other hand, Tsirelson's inequality says that for any ordered \*-ring we have `A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2√2` (A caveat: in the commutative case we need 2⁻¹ in the ring, @@ -49,9 +49,9 @@ To keep things simple we just assume our rings are ℝ-algebras.) The proofs I've seen in the literature either assume a significant framework for quantum mechanics, -or assume the ring is a `C^*`-algebra. -In the `C^*`-algebra case, -the order structure is completely determined by the `*`-algebra structure: +or assume the ring is a C⋆-algebra. +In the C⋆-algebra case, +the order structure is completely determined by the \*-algebra structure: `0 ≤ A` iff there exists some `B` so `A = star B * B`. There's a nice proof of both bounds in this setting at https://en.wikipedia.org/wiki/Tsirelson%27s_bound @@ -60,7 +60,7 @@ The proof given here is purely algebraic. ## Future work One can show that Tsirelson's inequality is tight. -In the `*`-ring of n-by-n complex matrices, if `A ≤ λ I` for some `λ : ℝ`, +In the \*-ring of n-by-n complex matrices, if `A ≤ λ I` for some `λ : ℝ`, then every eigenvalue has absolute value at most `λ`. There is a CHSH tuple in 4-by-4 matrices such that `A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁` has `2√2` as an eigenvalue. @@ -79,7 +79,7 @@ There is a CHSH tuple in 4-by-4 matrices such that universe u -/-- A CHSH tuple in a *-monoid consists of 4 self-adjoint involutions `A₀ A₁ B₀ B₁` such that +/-- A CHSH tuple in a \*-monoid consists of 4 self-adjoint involutions `A₀ A₁ B₀ B₁` such that the `Aᵢ` commute with the `Bⱼ`. The physical interpretation is that `A₀` and `A₁` are a pair of Boolean observables which @@ -107,7 +107,7 @@ theorem CHSH_id [CommRing R] {A₀ A₁ B₀ B₁ : R} (A₀_inv : A₀ ^ 2 = 1) 4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) := by grind -/-- Given a CHSH tuple (A₀, A₁, B₀, B₁) in a *commutative* ordered `*`-algebra over ℝ, +/-- Given a CHSH tuple (A₀, A₁, B₀, B₁) in a *commutative* ordered \*-algebra over ℝ, `A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2`. (We could work over ℤ[⅟2] if we wanted to!) @@ -152,7 +152,7 @@ end TsirelsonInequality open TsirelsonInequality -/-- In a noncommutative ordered `*`-algebra over ℝ, +/-- In a noncommutative ordered \*-algebra over ℝ, Tsirelson's bound for a CHSH tuple (A₀, A₁, B₀, B₁) is `A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2^(3/2) • 1`. diff --git a/Mathlib/Algebra/Star/CentroidHom.lean b/Mathlib/Algebra/Star/CentroidHom.lean index f52419f2d3bcd0..f1f448ba761453 100644 --- a/Mathlib/Algebra/Star/CentroidHom.lean +++ b/Mathlib/Algebra/Star/CentroidHom.lean @@ -15,7 +15,7 @@ public import Mathlib.Algebra.Star.Basic When a (nonunital, non-associative) semiring is equipped with an involutive automorphism the center of the centroid becomes a star ring in a natural way and the natural mapping of the centre of -the semiring into the centre of the centroid becomes a *-homomorphism. +the semiring into the centre of the centroid becomes a \*-homomorphism. ## Tags @@ -72,7 +72,7 @@ instance : StarRing (Subsemiring.center (CentroidHom α)) where _ = star (g (star (star (f (star a))))) := by simp only [star_star] _ = (star g * star f) a := rfl -/-- The canonical *-homomorphism embedding the center of `CentroidHom α` into `CentroidHom α`. -/ +/-- The canonical \*-homomorphism embedding the center of `CentroidHom α` into `CentroidHom α`. -/ def centerStarEmbedding : Subsemiring.center (CentroidHom α) →⋆ₙ+* CentroidHom α where toNonUnitalRingHom := (SubsemiringClass.subtype (Subsemiring.center (CentroidHom α))).toNonUnitalRingHom @@ -89,8 +89,8 @@ theorem star_centerToCentroidCenter (z : NonUnitalStarSubsemiring.center α) : _ = (star z) * a := by rw [(star z).property.comm] _ = (centerToCentroidCenter ((star z) : NonUnitalStarSubsemiring.center α)) a := rfl -/-- The canonical *-homomorphism from the center of a non-unital, non-associative *-semiring into -the center of its centroid. -/ +/-- The canonical \*-homomorphism from the center of a non-unital, non-associative \*-semiring +into the center of its centroid. -/ def starCenterToCentroidCenter : NonUnitalStarSubsemiring.center α →⋆ₙ+* Subsemiring.center (CentroidHom α) where toNonUnitalRingHom := centerToCentroidCenter diff --git a/Mathlib/Algebra/Star/Free.lean b/Mathlib/Algebra/Star/Free.lean index 6e80ddb99fea8a..e40a2fb5e44663 100644 --- a/Mathlib/Algebra/Star/Free.lean +++ b/Mathlib/Algebra/Star/Free.lean @@ -9,9 +9,9 @@ public import Mathlib.Algebra.Star.Basic public import Mathlib.Algebra.FreeAlgebra /-! -# A *-algebra structure on the free algebra. +# A \*-algebra structure on the free algebra. -Reversing words gives a *-structure on the free monoid or on the free algebra on a type. +Reversing words gives a \*-structure on the free monoid or on the free algebra on a type. ## Implementation note We have this in a separate file, rather than in `Algebra.FreeMonoid` and `Algebra.FreeAlgebra`, diff --git a/Mathlib/Algebra/Star/Rat.lean b/Mathlib/Algebra/Star/Rat.lean index 2ffa05b1726ab7..3d1f7e956ba853 100644 --- a/Mathlib/Algebra/Star/Rat.lean +++ b/Mathlib/Algebra/Star/Rat.lean @@ -11,7 +11,7 @@ public import Mathlib.Data.NNRat.Defs public import Mathlib.Data.Rat.Cast.Defs /-! -# *-ring structure on ℚ and ℚ≥0. +# \*-ring structure on `ℚ` and `ℚ≥0`. -/ @[expose] public section diff --git a/Mathlib/Algebra/Star/RingQuot.lean b/Mathlib/Algebra/Star/RingQuot.lean index 732c9d167e8ede..7bb4c00a742dea 100644 --- a/Mathlib/Algebra/Star/RingQuot.lean +++ b/Mathlib/Algebra/Star/RingQuot.lean @@ -9,7 +9,7 @@ public import Mathlib.Algebra.RingQuot public import Mathlib.Algebra.Star.Basic /-! -# The *-ring structure on suitable quotients of a *-ring. +# The \*-ring structure on suitable quotients of a \*-ring. -/ public section diff --git a/Mathlib/Algebra/Star/Subalgebra.lean b/Mathlib/Algebra/Star/Subalgebra.lean index 56ff8aa89c6ee7..d6f9dc04a2770e 100644 --- a/Mathlib/Algebra/Star/Subalgebra.lean +++ b/Mathlib/Algebra/Star/Subalgebra.lean @@ -13,16 +13,16 @@ public import Mathlib.Algebra.Star.NonUnitalSubalgebra /-! # Star subalgebras -A *-subalgebra is a subalgebra of a *-algebra which is closed under *. +A \*-subalgebra is a subalgebra of a \*-algebra which is closed under `*`. -The centralizer of a *-closed set is a *-subalgebra. +The centralizer of a \*-closed set is a \*-subalgebra. -/ @[expose] public section universe u v -/-- A *-subalgebra is a subalgebra of a *-algebra which is closed under *. -/ +/-- A \*-subalgebra is a subalgebra of a \*-algebra which is closed under `*`. -/ structure StarSubalgebra (R : Type u) (A : Type v) [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] : Type v extends Subalgebra R A where /-- The `carrier` is closed under the `star` operation. -/ @@ -30,7 +30,7 @@ structure StarSubalgebra (R : Type u) (A : Type v) [CommSemiring R] [StarRing R] namespace StarSubalgebra -/-- Forgetting that a *-subalgebra is closed under *. +/-- Forgetting that a \*-subalgebra is closed under \*. -/ add_decl_doc StarSubalgebra.toSubalgebra diff --git a/Mathlib/Algebra/Star/Subsemiring.lean b/Mathlib/Algebra/Star/Subsemiring.lean index 31c0525f59af92..9b53d8cd6c185d 100644 --- a/Mathlib/Algebra/Star/Subsemiring.lean +++ b/Mathlib/Algebra/Star/Subsemiring.lean @@ -11,7 +11,7 @@ public import Mathlib.Algebra.Ring.Subsemiring.Basic /-! # Star subrings -A *-subring is a subring of a *-ring which is closed under *. +A \*-subring is a subring of a \*-ring which is closed under `*`. -/ @[expose] public section diff --git a/Mathlib/Algebra/Star/Unitary.lean b/Mathlib/Algebra/Star/Unitary.lean index ca0cc415aae201..2d37c4b9fe8270 100644 --- a/Mathlib/Algebra/Star/Unitary.lean +++ b/Mathlib/Algebra/Star/Unitary.lean @@ -29,7 +29,7 @@ unitary @[expose] public section -/-- In a *-monoid, `unitary R` is the submonoid consisting of all the elements `U` of +/-- In a \*-monoid, `unitary R` is the submonoid consisting of all the elements `U` of `R` such that `star U * U = 1` and `U * star U = 1`. -/ def unitary (R : Type*) [Monoid R] [StarMul R] : Submonoid R where diff --git a/Mathlib/AlgebraicGeometry/Geometrically/Irreducible.lean b/Mathlib/AlgebraicGeometry/Geometrically/Irreducible.lean index 7e9d6a0723c9de..d52551a96300e8 100644 --- a/Mathlib/AlgebraicGeometry/Geometrically/Irreducible.lean +++ b/Mathlib/AlgebraicGeometry/Geometrically/Irreducible.lean @@ -15,7 +15,7 @@ public import Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen - `AlgebraicGeometry.GeometricallyIrreducible`: We say that morphism `f : X ⟶ Y` is geometrically irreducible if for all `Spec K ⟶ Y` with `K` a field, `X ×[Y] Spec K` is irreducible. - We also provide the fact that this is stable under base change (by infer_instance) + We also provide the fact that this is stable under base change (by `infer_instance`) - `GeometricallyIrreducible.iff_geometricallyIrreducible_fiber`: A scheme is geometrically irreducible over `S` iff the fibers of all `s : S` are geometrically irreducible. @@ -23,7 +23,7 @@ public import Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen If `X` is geometrically irreducible and universally open (e.g. when flat + finite presentation), over an irreducible scheme, then `X` is also irreducible. In particular, the base change of a geometrically irreducible and universally open scheme to an - irreducible scheme is irreducible (by infer_instance). + irreducible scheme is irreducible (by `infer_instance`). -/ universe u diff --git a/Mathlib/AlgebraicGeometry/Geometrically/Reduced.lean b/Mathlib/AlgebraicGeometry/Geometrically/Reduced.lean index 6a84959aea6a1f..0b9c8c8317db8a 100644 --- a/Mathlib/AlgebraicGeometry/Geometrically/Reduced.lean +++ b/Mathlib/AlgebraicGeometry/Geometrically/Reduced.lean @@ -16,7 +16,7 @@ public import Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant - `AlgebraicGeometry.GeometricallyReduced`: We say that morphism `f : X ⟶ Y` is geometrically reduced if for all `Spec K ⟶ Y` with `K` a field, `X ×[Y] Spec K` is reduced. - We also provide the fact that this is stable under base change (by infer_instance) + We also provide the fact that this is stable under base change (by `infer_instance`) - `GeometricallyReduced.iff_geometricallyReduced_fiber`: A scheme is geometrically reduced over `S` iff the fibers of all `s : S` are geometrically reduced. @@ -24,7 +24,7 @@ public import Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant If `X` is geometrically reduced and flat over a reduced and locally noetherian scheme, then `X` is also reduced. In particular, the base change of a geometrically reduced and flat scheme to an - reduced and locally noetherian scheme is reduced (by infer_instance). + reduced and locally noetherian scheme is reduced (by `infer_instance`). ## TODO Get rid of the noetherian assumption. diff --git a/Mathlib/AlgebraicGeometry/Sites/ConstantSheaf.lean b/Mathlib/AlgebraicGeometry/Sites/ConstantSheaf.lean index f0a55470b9f50e..a94470db8e8af7 100644 --- a/Mathlib/AlgebraicGeometry/Sites/ConstantSheaf.lean +++ b/Mathlib/AlgebraicGeometry/Sites/ConstantSheaf.lean @@ -107,7 +107,7 @@ def continuousMapPresheafAb (A : Type v) [TopologicalSpace A] [AddCommGroup A] variable (A : Type v) [TopologicalSpace A] [AddCommGroup A] [IsTopologicalAddGroup A] /-- `continuousMapPresheafAb` viewed as a type valued sheaf is isomorphic to -`continuousMapPresheaf. -/ +`continuousMapPresheaf`. -/ def continuousMapPresheafAbForgetIso : continuousMapPresheafAb A ⋙ CategoryTheory.forget Ab ≅ continuousMapPresheaf A := Iso.refl _ diff --git a/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean b/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean index 6aa49b6115f62a..ccf1050c9bc707 100644 --- a/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean +++ b/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean @@ -181,6 +181,7 @@ variable {X Y : TopCat.{u}} {f g : C(X, Y)} (H : ContinuousMap.Homotopy f g) {x /-! These definitions set up the following diagram, for each path `p`: +``` f(p) *--------* | \ | @@ -188,6 +189,7 @@ These definitions set up the following diagram, for each path `p`: | \ | *--------* g(p) +``` Here, `H₀ = H.evalAt x₀` is the path from `f(x₀)` to `g(x₀)`, and similarly for `H₁`. Similarly, `f(p)` denotes the diff --git a/Mathlib/AlgebraicTopology/SingularSet.lean b/Mathlib/AlgebraicTopology/SingularSet.lean index 4bf1fa40066830..f681694a1d8b48 100644 --- a/Mathlib/AlgebraicTopology/SingularSet.lean +++ b/Mathlib/AlgebraicTopology/SingularSet.lean @@ -104,7 +104,7 @@ noncomputable def TopCat.toSSetIsoConst (X : TopCat.{u}) [TotallyDisconnectedSpa ((TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace _ X).symm.trans (X.toSSetObjEquiv n).symm))).symm -/-- The canonical map `Δ[n] ⟶ Simp(Δₜ[n])` (where `Δₜ[n]` is the topological `n`-simplex`. -/ +/-- The canonical map `Δ[n] ⟶ Simp(Δₜ[n])` (where `Δₜ[n]` is the topological `n`-simplex). -/ @[simps! -isSimp] noncomputable def SSet.stdSimplexToTop : SSet.stdSimplex.{u} ⟶ SimplexCategory.toTop ⋙ TopCat.toSSet := SSet.stdSimplex.whiskerLeft sSetTopAdj.unit ≫ diff --git a/Mathlib/Analysis/CStarAlgebra/Basic.lean b/Mathlib/Analysis/CStarAlgebra/Basic.lean index bff53dd5834cce..1aa658ccd6fb40 100644 --- a/Mathlib/Analysis/CStarAlgebra/Basic.lean +++ b/Mathlib/Analysis/CStarAlgebra/Basic.lean @@ -30,7 +30,7 @@ Note that the type classes corresponding to C⋆-algebras are defined in ## TODO - Show that `‖x⋆ * x‖ = ‖x‖^2` is equivalent to `‖x⋆ * x‖ = ‖x⋆‖ * ‖x‖`, which is used as the - definition of C*-algebras in some sources (e.g. Wikipedia). + definition of C⋆-algebras in some sources (e.g. Wikipedia). -/ @@ -83,7 +83,7 @@ instance RingHomIsometric.starRingEnd [NormedCommRing E] [StarRing E] [NormedSta RingHomIsometric (starRingEnd E) := ⟨@norm_star _ _ _ _⟩ -/-- A C*-ring is a normed star ring that satisfies the stronger condition `‖x‖ ^ 2 ≤ ‖x⋆ * x‖` +/-- A C⋆-ring is a normed star ring that satisfies the stronger condition `‖x‖ ^ 2 ≤ ‖x⋆ * x‖` for every `x`. Note that this condition actually implies equality, as is shown in `norm_star_mul_self` below. -/ class CStarRing (E : Type*) [NonUnitalNormedRing E] [StarRing E] : Prop where @@ -111,7 +111,7 @@ lemma of_le_norm_mul_star_self variable [NonUnitalNormedRing E] [StarRing E] [CStarRing E] -- see Note [lower instance priority] -/-- In a C*-ring, star preserves the norm. -/ +/-- In a C⋆-ring, star preserves the norm. -/ instance (priority := 100) to_normedStarGroup : NormedStarGroup E where norm_star_le x := by obtain (hx | hx) := eq_zero_or_norm_pos x⋆ diff --git a/Mathlib/Analysis/Convex/Extreme.lean b/Mathlib/Analysis/Convex/Extreme.lean index ae6d59e33d3263..396323c12f3f72 100644 --- a/Mathlib/Analysis/Convex/Extreme.lean +++ b/Mathlib/Analysis/Convex/Extreme.lean @@ -144,7 +144,7 @@ theorem mem_extremePoints_iff_left : x ∈ A.extremePoints 𝕜 ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x := .rfl -/-- x is an extreme point to A iff {x} is an extreme set of A. -/ +/-- `x` is an extreme point to `A` iff `{x}` is an extreme set of `A`. -/ @[simp] lemma isExtreme_singleton : IsExtreme 𝕜 A {x} ↔ x ∈ A.extremePoints 𝕜 := by simp [isExtreme_iff, extremePoints] diff --git a/Mathlib/Analysis/Distribution/Sobolev.lean b/Mathlib/Analysis/Distribution/Sobolev.lean index e9512feb853839..fafaf2cbf74dcf 100644 --- a/Mathlib/Analysis/Distribution/Sobolev.lean +++ b/Mathlib/Analysis/Distribution/Sobolev.lean @@ -43,7 +43,7 @@ the definition of the Sobolev spaces. ## References * [M. Taylor, *Partial Differential Equations 1*][taylorPDE1] -* [W. McLean, *Strongly Elliptic Systems and Boundary Integral Equations][mclean2000] +* [W. McLean, *Strongly Elliptic Systems and Boundary Integral Equations*][mclean2000] -/ diff --git a/Mathlib/Analysis/InnerProductSpace/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Basic.lean index 58021d61e33ae6..a236bd98d9ceee 100644 --- a/Mathlib/Analysis/InnerProductSpace/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Basic.lean @@ -668,8 +668,7 @@ theorem dist_div_norm_sq_smul {x y : F} (hx : x ≠ 0) (hy : y ≠ 0) (R : ℝ) rw [sqrt_mul, sqrt_sq, sqrt_sq, dist_eq_norm] <;> positivity /-- The inner product of a nonzero vector with a nonzero multiple of -itself, divided by the product of their norms, has absolute value -1. -/ +itself, divided by the product of their norms, has absolute value 1. -/ theorem norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul {x : E} {r : 𝕜} (hx : x ≠ 0) (hr : r ≠ 0) : ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1 := by have hx' : ‖x‖ ≠ 0 := by simp [hx] @@ -679,8 +678,7 @@ theorem norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul {x : E} {r mul_div_cancel_right₀ _ hr', div_self hx'] /-- The inner product of a nonzero vector with a nonzero multiple of -itself, divided by the product of their norms, has absolute value -1. -/ +itself, divided by the product of their norms, has absolute value 1. -/ theorem abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul {x : F} {r : ℝ} (hx : x ≠ 0) (hr : r ≠ 0) : |⟪x, r • x⟫_ℝ| / (‖x‖ * ‖r • x‖) = 1 := norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/Reflection.lean b/Mathlib/Analysis/InnerProductSpace/Projection/Reflection.lean index e59e1b2c22616f..60a5da6f20eaaf 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection/Reflection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection/Reflection.lean @@ -129,7 +129,7 @@ theorem reflection_map {E E' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup reflection (K.map (f.toLinearEquiv : E →ₗ[𝕜] E')) = f.symm.trans (K.reflection.trans f) := LinearIsometryEquiv.ext <| reflection_map_apply f K -/-- Reflection through the trivial subspace {0} is just negation. -/ +/-- Reflection through the trivial subspace `{0}` is just negation. -/ @[simp] theorem reflection_bot : reflection (⊥ : Submodule 𝕜 E) = LinearIsometryEquiv.neg 𝕜 := by ext; simp [reflection_apply] diff --git a/Mathlib/Analysis/InnerProductSpace/Reproducing.lean b/Mathlib/Analysis/InnerProductSpace/Reproducing.lean index 6771855d8df8f6..e5afb58cb220c8 100644 --- a/Mathlib/Analysis/InnerProductSpace/Reproducing.lean +++ b/Mathlib/Analysis/InnerProductSpace/Reproducing.lean @@ -32,7 +32,7 @@ positive semidefinite matrices. ## References * [Paulsen, Vern I. and Raghupathi, Mrinal, - *An introduction to the theory of reproducing kernel {H}ilbert spaces*][MR3526117] + *An introduction to the theory of reproducing kernel Hilbert spaces*][MR3526117] -/ public noncomputable section diff --git a/Mathlib/Analysis/MeanInequalities.lean b/Mathlib/Analysis/MeanInequalities.lean index 925d4244e6abed..c1c851e769d2b2 100644 --- a/Mathlib/Analysis/MeanInequalities.lean +++ b/Mathlib/Analysis/MeanInequalities.lean @@ -149,7 +149,7 @@ theorem geom_mean_le_arith_mean_weighted (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 · simp [A i hi hz.symm] · rw [exp_log hz] -/-- **AM-GM inequality**: The **geometric mean is less than or equal to the arithmetic mean. -/ +/-- **AM-GM inequality**: The geometric mean is less than or equal to the arithmetic mean. -/ theorem geom_mean_le_arith_mean {ι : Type*} (s : Finset ι) (w : ι → ℝ) (z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : 0 < ∑ i ∈ s, w i) (hz : ∀ i ∈ s, 0 ≤ z i) : (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹ ≤ (∑ i ∈ s, w i * z i) / (∑ i ∈ s, w i) := by @@ -360,7 +360,7 @@ theorem harm_mean_le_geom_mean_weighted (w z : ι → ℝ) (hs : s.Nonempty) (hw · rw [Real.inv_rpow]; apply fun i hi ↦ le_of_lt (hz i hi); assumption -/-- **HM-GM inequality**: The **harmonic mean is less than or equal to the geometric mean. -/ +/-- **HM-GM inequality**: The harmonic mean is less than or equal to the geometric mean. -/ theorem harm_mean_le_geom_mean {ι : Type*} (s : Finset ι) (hs : s.Nonempty) (w : ι → ℝ) (z : ι → ℝ) (hw : ∀ i ∈ s, 0 < w i) (hw' : 0 < ∑ i ∈ s, w i) (hz : ∀ i ∈ s, 0 < z i) : (∑ i ∈ s, w i) / (∑ i ∈ s, w i / z i) ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹ := by diff --git a/Mathlib/Analysis/Meromorphic/Order.lean b/Mathlib/Analysis/Meromorphic/Order.lean index 274e3b9f5e6414..327418436de0f8 100644 --- a/Mathlib/Analysis/Meromorphic/Order.lean +++ b/Mathlib/Analysis/Meromorphic/Order.lean @@ -574,7 +574,7 @@ theorem meromorphicOrderAt_add (hf₁ : MeromorphicAt f₁ x) (hf₂ : Meromorph exact le_add_of_nonneg_right h₁g.meromorphicOrderAt_nonneg /-- -Helper lemma for meromorphicOrderAt_add_of_ne. +Helper lemma for `meromorphicOrderAt_add_of_ne`. -/ lemma meromorphicOrderAt_add_eq_left_of_lt (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x) : @@ -604,7 +604,7 @@ lemma meromorphicOrderAt_add_eq_left_of_lt (hf₂ : MeromorphicAt f₂ x) simp_all [smul_add, ← smul_assoc, ← zpow_add', sub_ne_zero] /-- -Helper lemma for meromorphicOrderAt_add_of_ne. +Helper lemma for `meromorphicOrderAt_add_of_ne`. -/ lemma meromorphicOrderAt_add_eq_right_of_lt (hf₁ : MeromorphicAt f₁ x) (h : meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x) : diff --git a/Mathlib/Analysis/Normed/Module/MStructure.lean b/Mathlib/Analysis/Normed/Module/MStructure.lean index 6ab84d6521d7e5..a07d3c7f5337d2 100644 --- a/Mathlib/Analysis/Normed/Module/MStructure.lean +++ b/Mathlib/Analysis/Normed/Module/MStructure.lean @@ -34,12 +34,12 @@ space with dual `X^*`. A closed subspace `M` of `X` is said to be an M-ideal if annihilator `M^∘` is an L-summand of `X^*`. M-ideal, M-summands and L-summands were introduced by Alfsen and Effros in [alfseneffros1972] to -study the structure of general Banach spaces. When `A` is a JB*-triple, the M-ideals of `A` are -exactly the norm-closed ideals of `A`. When `A` is a JBW*-triple with predual `X`, the M-summands of -`A` are exactly the weak*-closed ideals, and their pre-duals can be identified with the L-summands -of `X`. In the special case when `A` is a C*-algebra, the M-ideals are exactly the norm-closed -two-sided ideals of `A`, when `A` is also a W*-algebra the M-summands are exactly the weak*-closed -two-sided ideals of `A`. +study the structure of general Banach spaces. When `A` is a JB\*-triple, the M-ideals of `A` are +exactly the norm-closed ideals of `A`. When `A` is a JBW\*-triple with predual `X`, the M-summands +of `A` are exactly the weak\*-closed ideals, and their pre-duals can be identified with the +L-summands of `X`. In the special case when `A` is a C\*-algebra, the M-ideals are exactly the +norm-closed two-sided ideals of `A`, when `A` is also a W\*-algebra the M-summands are exactly the +weak\*-closed two-sided ideals of `A`. ## Implementation notes diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean index 9d2e4be266bab9..03e3b15b6832ad 100644 --- a/Mathlib/Analysis/Normed/Module/WeakDual.lean +++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean @@ -15,13 +15,13 @@ public import Mathlib.Analysis.LocallyConvex.WeakDual /-! # Weak dual of normed space -Let `E` be a normed space over a field `𝕜`. This file is concerned with properties of the weak-* +Let `E` be a normed space over a field `𝕜`. This file is concerned with properties of the weak-\* topology on the dual of `E`. By the dual, we mean either of the type synonyms `StrongDual 𝕜 E` or `WeakDual 𝕜 E`, depending on whether it is viewed as equipped with its usual -operator norm topology or the weak-* topology. +operator norm topology or the weak-\* topology. It is shown that the canonical mapping `StrongDual 𝕜 E → WeakDual 𝕜 E` is continuous, and -as a consequence the weak-* topology is coarser than the topology obtained from the operator norm +as a consequence the weak-\* topology is coarser than the topology obtained from the operator norm (dual norm). The file also equips `WeakDual 𝕜 E` with the norm bornology inherited from `StrongDual 𝕜 E`, so @@ -29,11 +29,11 @@ that `IsBounded` refers to operator-norm boundedness. This is a pragmatic choice further in the implementation notes. We establish the Banach-Alaoglu theorem about the compactness of closed balls in the dual of `E` -(as well as sets of somewhat more general form) with respect to the weak-* topology. +(as well as sets of somewhat more general form) with respect to the weak-\* topology. The first main result concerns the comparison of the operator norm topology on `StrongDual 𝕜 E` and -the weak-* topology on (its type synonym) `WeakDual 𝕜 E`: -* `dual_norm_topology_le_weak_dual_topology`: The weak-* topology on the dual of a normed space is +the weak-\* topology on (its type synonym) `WeakDual 𝕜 E`: +* `dual_norm_topology_le_weak_dual_topology`: The weak-\* topology on the dual of a normed space is coarser (not necessarily strictly) than the operator norm topology. * `WeakDual.isCompact_polar` (a version of the Banach-Alaoglu theorem): The polar set of a neighborhood of the origin in a normed space `E` over `𝕜` is compact in `WeakDual _ E`, if the @@ -46,22 +46,22 @@ the weak-* topology on (its type synonym) `WeakDual 𝕜 E`: * `StrongDual.toWeakDual` and `WeakDual.toStrongDual`: Linear equivalences between the dual types. * `WeakDual.instBornology`: The norm bornology on `WeakDual 𝕜 E`. -* `WeakDual.seminormFamily`: The family of seminorms `fun x f ↦ ‖f x‖` generating the weak-* +* `WeakDual.seminormFamily`: The family of seminorms `fun x f ↦ ‖f x‖` generating the weak-\* topology. * `WeakDual.polar`: The polar set of `s : Set E` viewed as a subset of `WeakDual 𝕜 E`. ## Main results ### Topology comparison -* `NormedSpace.Dual.toWeakDual_continuous`: The weak-* topology is coarser than the norm topology. +* `NormedSpace.Dual.toWeakDual_continuous`: The weak-\* topology is coarser than the norm topology. ### Bornology and pointwise bounds -* `WeakDual.isBounded_iff_isVonNBounded`: Equivalence of norm and weak-* boundedness for +* `WeakDual.isBounded_iff_isVonNBounded`: Equivalence of norm and weak-\* boundedness for Banach spaces. ### Compactness and Banach-Alaoglu -* `WeakDual.isCompact_polar`: Polars of neighborhoods of the origin are weak-* compact. -* `WeakDual.isCompact_closedBall`: Closed balls are weak-* compact. +* `WeakDual.isCompact_polar`: Polars of neighborhoods of the origin are weak-\* compact. +* `WeakDual.isCompact_closedBall`: Closed balls are weak-\* compact. * `WeakDual.isSeqCompact_closedBall`: Sequential version for separable spaces. ## Implementation notes @@ -75,19 +75,19 @@ the weak-* topology on (its type synonym) `WeakDual 𝕜 E`: 1. **Practicality:** In the normed setting, "bounded" is almost universally synonymous with "norm-bounded". This allows `IsBounded` to be used directly in statements like Banach-Alaoglu. 2. **Clarity:** It preserves a clear distinction between norm-boundedness (`IsBounded`) and - topological weak-* boundedness (`IsVonNBounded`). + topological weak-\* boundedness (`IsVonNBounded`). 3. **Consistency:** By the Uniform Boundedness Principle, these notions coincide whenever `E` is a Banach space (`isBounded_iff_isVonNBounded`). * **Polar sets:** The polar set `polar 𝕜 s` of a subset `s` of `E` is originally defined as a - subset of the dual `StrongDual 𝕜 E`. We care about properties of these w.r.t. weak-* topology, + subset of the dual `StrongDual 𝕜 E`. We care about properties of these w.r.t. weak-\* topology, and for this purpose give the definition `WeakDual.polar 𝕜 s` for the "same" subset viewed as a subset of `WeakDual 𝕜 E` (a type synonym of the dual but with a different topology instance). * **Banach-Alaoglu Proof:** The weak dual of `E` is embedded in the space of functions `E → 𝕜` with the topology of pointwise convergence. ## TODO -* Add that in finite dimensions, the weak-* topology and the dual norm topology coincide. -* Add that in infinite dimensions, the weak-* topology is strictly coarser than the dual norm +* Add that in finite dimensions, the weak-\* topology and the dual norm topology coincide. +* Add that in infinite dimensions, the weak-\* topology is strictly coarser than the dual norm topology. * Add metrizability of the dual unit ball (more generally weak-star compact subsets) of `WeakDual 𝕜 E` under the assumption of separability of `E`. @@ -148,9 +148,9 @@ end WeakDual /-! ### Weak star topology on duals of normed spaces -In this section, we prove properties about the weak-* topology on duals of normed spaces. +In this section, we prove properties about the weak-\* topology on duals of normed spaces. We prove in particular that the canonical mapping `StrongDual 𝕜 E → WeakDual 𝕜 E` is continuous, -i.e., that the weak-* topology is coarser (not necessarily strictly) than the topology given +i.e., that the weak-\* topology is coarser (not necessarily strictly) than the topology given by the dual-norm (i.e. the operator-norm). -/ @@ -186,7 +186,7 @@ open NormedSpace ### Bornology and pointwise bounds This section relates the inherited norm bornology (`IsBounded`) to the intrinsic -von Neumann bornology of the weak-* topology (`IsVonNBounded`). +von Neumann bornology of the weak-\* topology (`IsVonNBounded`). The following results justify using the norm bornology as the default instance: by the Uniform Boundedness Principle, it coincides with the von Neumann bornology whenever @@ -195,7 +195,7 @@ $E$ is a Banach space. variable (𝕜 E) in /-- The family of seminorms on `WeakDual 𝕜 E` given by `fun x f ↦ ‖f x‖`, indexed by `E`. -This is the seminorm family associated to the weak-* topology via `topDualPairing`. -/ +This is the seminorm family associated to the weak-\* topology via `topDualPairing`. -/ def seminormFamily : SeminormFamily 𝕜 (WeakDual 𝕜 E) E := (topDualPairing 𝕜 E).toSeminormFamily @[simp] @@ -254,8 +254,8 @@ theorem isBounded_closedBall (x' : StrongDual 𝕜 E) (r : ℝ) : IsBounded (toStrongDual ⁻¹' closedBall x' r) := isBounded_toStrongDual_preimage_iff_isBounded.mpr Metric.isBounded_closedBall -/-- The weak-* closure of a norm-bounded set is norm-bounded, because norm-closed balls -are weak-* closed. -/ +/-- The weak-\* closure of a norm-bounded set is norm-bounded, because norm-closed balls +are weak-\* closed. -/ theorem isBounded_closure {s : Set (WeakDual 𝕜 E)} (hb : IsBounded s) : IsBounded (closure s) := by obtain ⟨R, hR⟩ := (Metric.isBounded_iff_subset_closedBall (0 : StrongDual 𝕜 E)).mp hb @@ -363,7 +363,7 @@ theorem isSeqCompact_polar {s : Set E} (s_nhd : s ∈ 𝓝 (0 : E)) : isSeqCompact_of_isBounded_of_isClosed 𝕜 _ (isBounded_polar 𝕜 s_nhd) (isClosed_polar _ _) /-- The **Sequential Banach-Alaoglu theorem**: closed balls of the dual of a separable -normed space `V` are sequentially compact in the weak-* topology. -/ +normed space `V` are sequentially compact in the weak-\* topology. -/ theorem isSeqCompact_closedBall (x' : StrongDual 𝕜 E) (r : ℝ) : IsSeqCompact (toStrongDual ⁻¹' Metric.closedBall x' r) := isSeqCompact_of_isBounded_of_isClosed 𝕜 _ (isBounded_closedBall x' r) (isClosed_closedBall x' r) diff --git a/Mathlib/Analysis/Normed/Operator/Completeness.lean b/Mathlib/Analysis/Normed/Operator/Completeness.lean index 080b5755b29918..be6f7c91184b71 100644 --- a/Mathlib/Analysis/Normed/Operator/Completeness.lean +++ b/Mathlib/Analysis/Normed/Operator/Completeness.lean @@ -107,9 +107,9 @@ theorem isCompact_image_coe_of_bounded_of_closed_image [ProperSpace F] {s : Set IsCompact (((↑) : (E' →SL[σ₁₂] F) → E' → F) '' s) := hc.closure_eq ▸ isCompact_closure_image_coe_of_bounded hb -/-- If a set `s` of semilinear functions is bounded and is closed in the weak-* topology, then its +/-- If a set `s` of semilinear functions is bounded and is closed in the weak-\* topology, then its image under coercion to functions `E → F` is a closed set. We don't have a name for `E →SL[σ] F` -with weak-* topology in `mathlib`, so we use an equivalent condition (see `isClosed_induced_iff'`). +with weak-\* topology in `mathlib`, so we use an equivalent condition (see `isClosed_induced_iff'`). TODO: reformulate this in terms of a type synonym with the right topology. -/ theorem isClosed_image_coe_of_bounded_of_weak_closed {s : Set (E' →SL[σ₁₂] F)} (hb : IsBounded s) @@ -119,9 +119,9 @@ theorem isClosed_image_coe_of_bounded_of_weak_closed {s : Set (E' →SL[σ₁₂ isClosed_of_closure_subset fun f hf => ⟨ofMemClosureImageCoeBounded f hb hf, hc (ofMemClosureImageCoeBounded f hb hf) hf, rfl⟩ -/-- If a set `s` of semilinear functions is bounded and is closed in the weak-* topology, then its +/-- If a set `s` of semilinear functions is bounded and is closed in the weak-\* topology, then its image under coercion to functions `E → F` is a compact set. We don't have a name for `E →SL[σ] F` -with weak-* topology in `mathlib`, so we use an equivalent condition (see `isClosed_induced_iff'`). +with weak-\* topology in `mathlib`, so we use an equivalent condition (see `isClosed_induced_iff'`). -/ theorem isCompact_image_coe_of_bounded_of_weak_closed [ProperSpace F] {s : Set (E' →SL[σ₁₂] F)} (hb : IsBounded s) (hc : ∀ f : E' →SL[σ₁₂] F, @@ -130,8 +130,8 @@ theorem isCompact_image_coe_of_bounded_of_weak_closed [ProperSpace F] {s : Set ( isCompact_image_coe_of_bounded_of_closed_image hb <| isClosed_image_coe_of_bounded_of_weak_closed hb hc -/-- A closed ball is closed in the weak-* topology. We don't have a name for `E →SL[σ] F` with -weak-* topology in `mathlib`, so we use an equivalent condition (see `isClosed_induced_iff'`). -/ +/-- A closed ball is closed in the weak-\* topology. We don't have a name for `E →SL[σ] F` with +weak-\* topology in `mathlib`, so we use an equivalent condition (see `isClosed_induced_iff'`). -/ theorem is_weak_closed_closedBall (f₀ : E' →SL[σ₁₂] F) (r : ℝ) ⦃f : E' →SL[σ₁₂] F⦄ (hf : ⇑f ∈ closure (((↑) : (E' →SL[σ₁₂] F) → E' → F) '' closedBall f₀ r)) : f ∈ closedBall f₀ r := by diff --git a/Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean b/Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean index 59158fd8c39104..18ddef50b9bccb 100644 --- a/Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean +++ b/Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean @@ -204,10 +204,10 @@ lemma deriv_binEntropy (p : ℝ) : deriv binEntropy p = log (1 - p) - log p := b /-- Shannon q-ary Entropy function (measured in Nats, i.e., using natural logs). -It's the Shannon entropy of a random variable with possible outcomes {1, ..., q} +It's the Shannon entropy of a random variable with possible outcomes `{1, ..., q}` where outcome `1` has probability `1 - p` and all other outcomes are equally likely. -The usual domain of definition is p ∈ [0,1], i.e., input is a probability. +The usual domain of definition is `p ∈ [0,1]`, i.e., input is a probability. This is a generalization of the binary entropy function `binEntropy`. -/ @[pp_nodot] noncomputable def qaryEntropy (q : ℕ) (p : ℝ) : ℝ := p * log (q - 1 : ℤ) + binEntropy p diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean index 15d1e7865cd4ab..494efbc07e25bd 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean @@ -22,13 +22,13 @@ Chebyshev T polynomials are orthogonal with respect to `√(1 - x ^ 2)⁻¹`. ## Main statements -* integrable_measureT: continuous functions are integrable with respect to Lebesgue measure +* `integrable_measureT`: continuous functions are integrable with respect to Lebesgue measure scaled by `√(1 - x ^ 2)⁻¹` and restricted to `(-1, 1]`. -* integral_eval_T_real_mul_evalT_real_measureT_of_ne: +* `integral_eval_T_real_mul_evalT_real_measureT_of_ne`: if `n ≠ m` then the integral of `T_n * T_m` equals `0`. -* integral_eval_T_real_mul_self_measureT_zero: +* `integral_eval_T_real_mul_self_measureT_zero`: if `n = m = 0` then the integral equals `π`. -* integral_eval_T_real_mul_self_measureT_of_ne_zero: +* `integral_eval_T_real_mul_self_measureT_of_ne_zero`: if `n = m ≠ 0` then the integral equals `π / 2`. ## TODO diff --git a/Mathlib/Analysis/VonNeumannAlgebra/Basic.lean b/Mathlib/Analysis/VonNeumannAlgebra/Basic.lean index 207ebc47f9a386..1c2176cf7a8c21 100644 --- a/Mathlib/Analysis/VonNeumannAlgebra/Basic.lean +++ b/Mathlib/Analysis/VonNeumannAlgebra/Basic.lean @@ -14,14 +14,14 @@ public import Mathlib.Analysis.InnerProductSpace.Adjoint We give the "abstract" and "concrete" definitions of a von Neumann algebra. We still have a major project ahead of us to show the equivalence between these definitions! -An abstract von Neumann algebra `WStarAlgebra M` is a C^* algebra with a Banach space predual, +An abstract von Neumann algebra `WStarAlgebra M` is a C⋆ algebra with a Banach space predual, per Sakai (1971). A concrete von Neumann algebra `VonNeumannAlgebra H` (where `H` is a Hilbert space) -is a *-closed subalgebra of bounded operators on `H` which is equal to its double commutant. +is a \*-closed subalgebra of bounded operators on `H` which is equal to its double commutant. We'll also need to prove the von Neumann double commutant theorem, -that the concrete definition is equivalent to a *-closed subalgebra which is weakly closed. +that the concrete definition is equivalent to a \*-closed subalgebra which is weakly closed. -/ @[expose] public section @@ -29,16 +29,16 @@ that the concrete definition is equivalent to a *-closed subalgebra which is wea universe u v -/-- Sakai's definition of a von Neumann algebra as a C^* algebra with a Banach space predual. +/-- Sakai's definition of a von Neumann algebra as a C⋆ algebra with a Banach space predual. So that we can unambiguously talk about these "abstract" von Neumann algebras -in parallel with the "concrete" ones (weakly closed *-subalgebras of B(H)), +in parallel with the "concrete" ones (weakly closed \*-subalgebras of B(H)), we name this definition `WStarAlgebra`. Note that for now we only assert the mere existence of predual, rather than picking one. This may later prove problematic, and need to be revisited. Picking one may cause problems with definitional unification of different instances. -One the other hand, not picking one means that the weak-* topology +One the other hand, not picking one means that the weak-\* topology (which depends on a choice of predual) must be defined using the choice, and we may be unhappy with the resulting opaqueness of the definition. -/ @@ -51,12 +51,12 @@ class WStarAlgebra (M : Type u) [CStarAlgebra M] : Prop where -- TODO: Without this, `VonNeumannAlgebra` times out. Why? /-- The double commutant definition of a von Neumann algebra, -as a *-closed subalgebra of bounded operators on a Hilbert space, +as a \*-closed subalgebra of bounded operators on a Hilbert space, which is equal to its double commutant. Note that this definition is parameterised by the Hilbert space on which the algebra faithfully acts, as is standard in the literature. -See `WStarAlgebra` for the abstract notion (a C^*-algebra with Banach space predual). +See `WStarAlgebra` for the abstract notion (a C⋆-algebra with Banach space predual). Note this is a bundled structure, parameterised by the Hilbert space `H`, rather than a typeclass on the type of elements. @@ -69,7 +69,7 @@ structure VonNeumannAlgebra (H : Type u) [NormedAddCommGroup H] [InnerProductSpa /-- The double commutant (a.k.a. centralizer) of a `VonNeumannAlgebra` is itself. -/ centralizer_centralizer' : Set.centralizer (Set.centralizer carrier) = carrier -/-- Consider a von Neumann algebra acting on a Hilbert space `H` as a *-subalgebra of `H →L[ℂ] H`. +/-- Consider a von Neumann algebra acting on a Hilbert space `H` as a \*-subalgebra of `H →L[ℂ] H`. (That is, we forget that it is equal to its double commutant or equivalently that it is closed in the weak and strong operator topologies.) -/ diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean index f91b26d69223e4..491f7a78ceed18 100644 --- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean +++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean @@ -241,7 +241,7 @@ instance (priority := 100) [HasCoproducts.{w} C] [AB4OfSize.{w} C] : haveI : HasCoproducts.{0} C := hasCoproducts_shrink AB4OfSize.{0} C := AB4OfSize_shrink C -/-- A category `C` which has products is said to have `AB4Star` (in literature `AB4*`) +/-- A category `C` which has products is said to have `AB4Star` (in literature AB4\*) provided that products are exact. -/ @[pp_with_univ, stacks 079B] class AB4StarOfSize [HasProducts.{w} C] where @@ -249,7 +249,7 @@ class AB4StarOfSize [HasProducts.{w} C] where attribute [instance] AB4StarOfSize.ofShape -/-- A category `C` which has products is said to have `AB4Star` (in literature `AB4*`) +/-- A category `C` which has products is said to have `AB4Star` (in literature AB4\*) provided that products are exact. -/ abbrev AB4Star [HasProducts C] := AB4StarOfSize.{v} C @@ -467,7 +467,7 @@ lemma AB4Star.of_AB5Star [HasCofilteredLimitsOfSize.{w, w} C] [AB5StarOfSize.{w, ofShape _ := hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op _ _ /-- -A category with finite biproducts and finite limits has countable AB4* if sequential limits are +A category with finite biproducts and finite limits has countable AB4\* if sequential limits are exact. -/ lemma CountableAB4Star.of_countableAB5Star [HasLimitsOfShape ℕᵒᵖ C] [HasExactLimitsOfShape ℕᵒᵖ C] @@ -500,7 +500,7 @@ lemma CountableAB4.of_hasExactColimitsOfShape_nat_and_finite [HasCountableCoprod /-- Checking exactness of limits of shape `Discrete ℕ` and `Discrete J` for finite `J` is enough for -countable AB4*. +countable AB4\*. -/ lemma CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite [HasCountableProducts C] [HasFiniteColimits C] [∀ (J : Type) [Finite J], HasExactLimitsOfShape (Discrete J) C] @@ -540,7 +540,7 @@ lemma CountableAB4.of_hasExactColimitsOfShape_nat [HasFiniteLimits C] [HasCounta exact fun _ ↦ inferInstance /-- -Checking exact limits of shape `Discrete ℕ` is enough for countable AB4*, provided that the +Checking exact limits of shape `Discrete ℕ` is enough for countable AB4\*, provided that the category has finite biproducts and finite colimits. -/ lemma CountableAB4Star.of_hasExactLimitsOfShape_nat [HasFiniteColimits C] diff --git a/Mathlib/CategoryTheory/Abelian/Preradical/Colon.lean b/Mathlib/CategoryTheory/Abelian/Preradical/Colon.lean index b8f41c1e099087..dbcd2af4be66ba 100644 --- a/Mathlib/CategoryTheory/Abelian/Preradical/Colon.lean +++ b/Mathlib/CategoryTheory/Abelian/Preradical/Colon.lean @@ -37,7 +37,7 @@ quotients in the sense that `Φ.quotient ⋙ Ψ.r` is the zero object. ## Tags -category_theory, preradical, colon, pullback, torsion theory +category theory, preradical, colon, pullback, torsion theory -/ @[expose] public section diff --git a/Mathlib/CategoryTheory/CodiscreteCategory.lean b/Mathlib/CategoryTheory/CodiscreteCategory.lean index b2ebef7ed87b6d..98c642d72e5e70 100644 --- a/Mathlib/CategoryTheory/CodiscreteCategory.lean +++ b/Mathlib/CategoryTheory/CodiscreteCategory.lean @@ -87,8 +87,8 @@ def natIso {F G : C ⥤ Codiscrete A} : F ≅ G where hom := natTrans inv := natTrans -/-- Every functor `F` to a codiscrete category is naturally isomorphic {(actually, equal)} to - `Codiscrete.as ∘ F.obj`. -/ +/-- Every functor `F` to a codiscrete category is naturally isomorphic (actually, equal) to +`Codiscrete.as ∘ F.obj`. -/ @[simps!] def natIsoFunctor {F : C ⥤ Codiscrete A} : F ≅ functor (Codiscrete.as ∘ F.obj) := Iso.refl _ diff --git a/Mathlib/CategoryTheory/EffectiveEpi/Enough.lean b/Mathlib/CategoryTheory/EffectiveEpi/Enough.lean index eda409c9eb3a5f..d4d07cc3c27cfe 100644 --- a/Mathlib/CategoryTheory/EffectiveEpi/Enough.lean +++ b/Mathlib/CategoryTheory/EffectiveEpi/Enough.lean @@ -37,7 +37,7 @@ structure EffectivePresentation (X : D) where effectiveEpi : EffectiveEpi f /-- -`D` has *effectively enough objects with respect to the functor `F` if every object has an +`D` has *effectively enough objects* with respect to the functor `F` if every object has an effective presentation. -/ class EffectivelyEnough : Prop where diff --git a/Mathlib/CategoryTheory/Functor/Const.lean b/Mathlib/CategoryTheory/Functor/Const.lean index 904a6aaa29d6c7..b608cfcfbbf787 100644 --- a/Mathlib/CategoryTheory/Functor/Const.lean +++ b/Mathlib/CategoryTheory/Functor/Const.lean @@ -83,7 +83,7 @@ section variable {D : Type u₃} [Category.{v₃} D] /-- These are actually equal, of course, but not definitionally equal - (the equality requires F.map (𝟙 _) = 𝟙 _). A natural isomorphism is + (the equality requires `F.map (𝟙 _) = 𝟙 _`). A natural isomorphism is more convenient than an equality between functors (compare id_to_iso). -/ @[simps] def constComp (X : C) (F : C ⥤ D) : (const J).obj X ⋙ F ≅ (const J).obj (F.obj X) where diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean index b7cbe3dbd02c8a..f4899e912d77b8 100644 --- a/Mathlib/CategoryTheory/Limits/HasLimits.lean +++ b/Mathlib/CategoryTheory/Limits/HasLimits.lean @@ -393,7 +393,7 @@ theorem limit.pre_pre [h : HasLimit (D ⋙ E ⋙ F)] : haveI : HasLimit ((D ⋙ variable {E F} set_option backward.isDefEq.respectTransparency false in -/-- - +/-- If we have particular limit cones available for `E ⋙ F` and for `F`, we obtain a formula for `limit.pre F E`. -/ @@ -965,7 +965,7 @@ theorem colimit.pre_pre [h : HasColimit (D ⋙ E ⋙ F)] : variable {E F} set_option backward.isDefEq.respectTransparency false in -/-- - +/-- If we have particular colimit cocones available for `E ⋙ F` and for `F`, we obtain a formula for `colimit.pre F E`. -/ diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean index 42fb69b209c099..1cdad676898b3c 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean @@ -14,7 +14,7 @@ public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback This file defines (co)equalizers as special cases of (co)limits. -An equalizer is the categorical generalization of the subobject {a ∈ A | f(a) = g(a)} known +An equalizer is the categorical generalization of the subobject ${a ∈ A | f(a) = g(a)}$ known from abelian groups or modules. It is a limit cone over the diagram formed by `f` and `g`. A coequalizer is the dual concept. diff --git a/Mathlib/CategoryTheory/Monad/Basic.lean b/Mathlib/CategoryTheory/Monad/Basic.lean index 854258c393b2fa..a81dec24df1974 100644 --- a/Mathlib/CategoryTheory/Monad/Basic.lean +++ b/Mathlib/CategoryTheory/Monad/Basic.lean @@ -35,10 +35,10 @@ universe v₁ u₁ variable (C : Type u₁) [Category.{v₁} C] /-- The data of a monad on C consists of an endofunctor T together with natural transformations -η : 𝟭 C ⟶ T and μ : T ⋙ T ⟶ T satisfying three equations: -- T μ_X ≫ μ_X = μ_(TX) ≫ μ_X (associativity) -- η_(TX) ≫ μ_X = 1_X (left unit) -- Tη_X ≫ μ_X = 1_X (right unit) +`η : 𝟭 C ⟶ T` and `μ : T ⋙ T ⟶ T` satisfying three equations: +- `T μ_X ≫ μ_X = μ_(TX) ≫ μ_X` (associativity) +- `η_(TX) ≫ μ_X = 1_X` (left unit) +- `Tη_X ≫ μ_X = 1_X` (right unit) -/ structure Monad extends C ⥤ C where /-- The unit for the monad. -/ @@ -60,10 +60,10 @@ lemma Monad.mu_naturality (T : Monad C) ⦃X Y : C⦄ (f : X ⟶ Y) : T.μ.naturality _ /-- The data of a comonad on C consists of an endofunctor G together with natural transformations -ε : G ⟶ 𝟭 C and δ : G ⟶ G ⋙ G satisfying three equations: -- δ_X ≫ G δ_X = δ_X ≫ δ_(GX) (coassociativity) -- δ_X ≫ ε_(GX) = 1_X (left counit) -- δ_X ≫ G ε_X = 1_X (right counit) +`ε : G ⟶ 𝟭 C` and `δ : G ⟶ G ⋙ G` satisfying three equations: +- `δ_X ≫ G δ_X = δ_X ≫ δ_(GX)` (coassociativity) +- `δ_X ≫ ε_(GX) = 1_X` (left counit) +- `δ_X ≫ G ε_X = 1_X` (right counit) -/ structure Comonad extends C ⥤ C where /-- The counit for the comonad. -/ diff --git a/Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean index 6c8b1904200b76..d44d6b67192c33 100644 --- a/Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean +++ b/Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean @@ -395,8 +395,8 @@ lemma comp_eq (x y z : C) [Closed x] [Closed y] : comp x y z = curry (compTransp /-! The proofs of associativity and unitality use the following outline: - 1. Take adjoint transpose on each side of the equality (uncurry_injective) - 2. Do whatever rewrites/simps are necessary to apply uncurry_curry + 1. Take adjoint transpose on each side of the equality (`uncurry_injective`) + 2. Do whatever rewrites/simps are necessary to apply `uncurry_curry` 3. Conclude with simp -/ diff --git a/Mathlib/CategoryTheory/Monoidal/Mod_.lean b/Mathlib/CategoryTheory/Monoidal/Mod_.lean index 3d3e00d20a6f10..642b5dedc57bb4 100644 --- a/Mathlib/CategoryTheory/Monoidal/Mod_.lean +++ b/Mathlib/CategoryTheory/Monoidal/Mod_.lean @@ -141,7 +141,7 @@ structure Hom (M N : Mod_ D A) where attribute [instance] Hom.isMod_Hom /-- An alternative constructor for `Hom`, -taking a morphism without a [isMod_Hom] instance, as well as the relevant +taking a morphism without a `[isMod_Hom]` instance, as well as the relevant equality to put such an instance. -/ @[simps!] def Hom.mk' {M N : Mod_ D A} (f : M.X ⟶ N.X) @@ -150,7 +150,7 @@ def Hom.mk' {M N : Mod_ D A} (f : M.X ⟶ N.X) ⟨f⟩ /-- An alternative constructor for `Hom`, -taking a morphism without a [isMod_Hom] instance, between objects with +taking a morphism without a `[isMod_Hom]` instance, between objects with a `ModObj` instance (rather than bundled as `Mod_`), as well as the relevant equality to put such an instance. -/ @[simps!] diff --git a/Mathlib/CategoryTheory/Monoidal/Rigid/Braided.lean b/Mathlib/CategoryTheory/Monoidal/Rigid/Braided.lean index e8d7562fe515b3..8631273bd73480 100644 --- a/Mathlib/CategoryTheory/Monoidal/Rigid/Braided.lean +++ b/Mathlib/CategoryTheory/Monoidal/Rigid/Braided.lean @@ -21,7 +21,7 @@ variable {C : Type*} [Category* C] [MonoidalCategory C] [BraidedCategory C] {X Y namespace CategoryTheory.BraidedCategory set_option backward.privateInPublic true in -/-- coevaluation_evaluation' field of `ExactPairing Y X` in a braided category -/ +/-- `coevaluation_evaluation'` field of `ExactPairing Y X` in a braided category -/ private theorem coevaluation_evaluation_braided' [inst : ExactPairing X Y] : X ◁ (η_ X Y ≫ (β_ Y X).inv) ≫ (α_ X Y X).inv ≫ ((β_ X Y).hom ≫ ε_ X Y) ▷ X = (ρ_ X).hom ≫ (λ_ X).inv := by @@ -48,7 +48,7 @@ private theorem coevaluation_evaluation_braided' [inst : ExactPairing X Y] : simp [monoidalComp] set_option backward.privateInPublic true in -/-- evaluation_coevaluation' field of `ExactPairing Y X` in a braided category -/ +/-- `evaluation_coevaluation'` field of `ExactPairing Y X` in a braided category -/ private theorem evaluation_coevaluation_braided' [inst : ExactPairing X Y] : (η_ X Y ≫ (β_ Y X).inv) ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ ((β_ X Y).hom ≫ ε_ X Y) = (λ_ Y).hom ≫ (ρ_ Y).inv := by diff --git a/Mathlib/CategoryTheory/NatIso.lean b/Mathlib/CategoryTheory/NatIso.lean index ecba0bc9214f52..abdff0d1354332 100644 --- a/Mathlib/CategoryTheory/NatIso.lean +++ b/Mathlib/CategoryTheory/NatIso.lean @@ -15,14 +15,13 @@ For the most part, natural isomorphisms are just another sort of isomorphism. We provide some special support for extracting components: * if `α : F ≅ G`, then `α.app X : F.obj X ≅ G.obj X`, and building natural isomorphisms from components: -* -``` -NatIso.ofComponents - (app : ∀ X : C, F.obj X ≅ G.obj X) - (naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) : -F ≅ G -``` -only needing to check naturality in one direction. +* ``` + NatIso.ofComponents + (app : ∀ X : C, F.obj X ≅ G.obj X) + (naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) : + F ≅ G + ``` + only needing to check naturality in one direction. ## Implementation diff --git a/Mathlib/CategoryTheory/Sites/IsSheafFor.lean b/Mathlib/CategoryTheory/Sites/IsSheafFor.lean index 424278685e8553..4573627243f011 100644 --- a/Mathlib/CategoryTheory/Sites/IsSheafFor.lean +++ b/Mathlib/CategoryTheory/Sites/IsSheafFor.lean @@ -643,7 +643,7 @@ theorem isSheafFor_iff_generate (R : Presieve X) : intro t ht simpa [hx] using isAmalgamation_restrict (le_generate R) _ _ ht -/-- Every presheaf is a sheaf for the family {𝟙 X}. +/-- Every presheaf is a sheaf for the family `{𝟙 X}`. [Elephant] C2.1.5(i) -/ diff --git a/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean b/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean index fda48de3ba998d..fdacae8f232a4b 100644 --- a/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean +++ b/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean @@ -29,7 +29,7 @@ inequality. ## References * [Giorgis Petridis, *The Plünnecke-Ruzsa inequality: an overview*][petridis2014] -* [Terence Tao, Van Vu, *Additive Combinatorics][tao-vu] +* [Terence Tao, Van Vu, *Additive Combinatorics*][tao-vu] ## See also diff --git a/Mathlib/Combinatorics/Schnirelmann.lean b/Mathlib/Combinatorics/Schnirelmann.lean index 327e6d5997b979..c9abdee1ad31e8 100644 --- a/Mathlib/Combinatorics/Schnirelmann.lean +++ b/Mathlib/Combinatorics/Schnirelmann.lean @@ -50,7 +50,7 @@ which reduces the proof obligations later that would arise with `Nat.card`. open Finset -/-- The Schnirelmann density is defined as the infimum of |A ∩ {1, ..., n}| / n as n ranges over +/-- The Schnirelmann density is defined as the infimum of $|A ∩ {1, ..., n}| / n$ as n ranges over the positive naturals. -/ noncomputable def schnirelmannDensity (A : Set ℕ) [DecidablePred (· ∈ A)] : ℝ := ⨅ n : {n : ℕ // 0 < n}, #{a ∈ Ioc 0 n | a ∈ A} / n diff --git a/Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean b/Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean index f3c8dda0a5de56..f514272152c906 100644 --- a/Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean +++ b/Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean @@ -41,11 +41,13 @@ The first interesting cases of such structures are `W₁,₀` and `W₂,₁`: `W while `W₂,₁` is a 5-cycle with an extra central hub vertex adjacent to all other vertices (i.e. `W₂,₁` resembles a wheel with five spokes). +``` `W₁,₀` v `W₂,₁` v / \ / | \ s t s ─ u ─ t \ / \ / \ / w₁ ─ w₂ w₁ ─ w₂ +``` ## Main definitions diff --git a/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean b/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean index a738cd02694c1f..a700cb47768a8e 100644 --- a/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean +++ b/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean @@ -15,8 +15,8 @@ import Mathlib.Algebra.Order.Interval.Set.Group This file defines and develops an API for the polynomial growth condition that appears in the statement of the Akra-Bazzi theorem: for the theorem to hold, the function `g` must -satisfy the condition that `c₁ g(n) ≤ g(u) ≤ c₂ g(n)`, for u between b*n and n for any constant -`b ∈ (0,1)`. +satisfy the condition that `c₁ g(n) ≤ g(u) ≤ c₂ g(n)`, for `u` between `b*n` and `n` for any +constant `b ∈ (0,1)`. ## Implementation notes diff --git a/Mathlib/Computability/RegularExpressions.lean b/Mathlib/Computability/RegularExpressions.lean index f1f698c89062b7..4b3887a7e7eb32 100644 --- a/Mathlib/Computability/RegularExpressions.lean +++ b/Mathlib/Computability/RegularExpressions.lean @@ -36,7 +36,7 @@ variable {α β γ : Type*} set_option genSizeOfSpec false in set_option genInjectivity false in /-- This is the definition of regular expressions. The names used here are meant to mirror the -definition of a Kleene algebra (https://en.wikipedia.org/wiki/Kleene_algebra). +[definition of a Kleene algebra](https://en.wikipedia.org/wiki/Kleene_algebra). * `0` (`zero`) matches nothing * `1` (`epsilon`) matches only the empty string * `char a` matches only the string 'a' diff --git a/Mathlib/Computability/TuringMachine/ToPartrec.lean b/Mathlib/Computability/TuringMachine/ToPartrec.lean index 7ac1eb9c5932a7..210b97f4e9d17c 100644 --- a/Mathlib/Computability/TuringMachine/ToPartrec.lean +++ b/Mathlib/Computability/TuringMachine/ToPartrec.lean @@ -402,10 +402,12 @@ def trCont : Cont → Cont' /-- We use `PosNum` to define the translation of binary natural numbers. A natural number is represented as a little-endian list of `bit0` and `bit1` elements: +``` 1 = [bit1] 2 = [bit0, bit1] 3 = [bit1, bit1] 4 = [bit0, bit0, bit1] +``` In particular, this representation guarantees no trailing `bit0`'s at the end of the list. -/ def trPosNum : PosNum → List Γ' @@ -417,11 +419,13 @@ def trPosNum : PosNum → List Γ' translated using `trPosNum`, and `trNum 0 = []`. So there are never any trailing `bit0`'s in a translated `Num`. +``` 0 = [] 1 = [bit1] 2 = [bit0, bit1] 3 = [bit1, bit1] 4 = [bit0, bit0, bit1] +``` -/ def trNum : Num → List Γ' | Num.zero => [] diff --git a/Mathlib/Condensed/AB.lean b/Mathlib/Condensed/AB.lean index 50af34e40052f1..45d72df3a101ac 100644 --- a/Mathlib/Condensed/AB.lean +++ b/Mathlib/Condensed/AB.lean @@ -15,7 +15,7 @@ public import Mathlib.Condensed.Limits # AB axioms in condensed modules This file proves that the category of condensed modules over a ring satisfies Grothendieck's axioms -AB5, AB4, and AB4*. +AB5, AB4, and AB4`*`. -/ @[expose] public section diff --git a/Mathlib/Condensed/Light/AB.lean b/Mathlib/Condensed/Light/AB.lean index a37fa8b40b09cd..7d25f174122ed3 100644 --- a/Mathlib/Condensed/Light/AB.lean +++ b/Mathlib/Condensed/Light/AB.lean @@ -8,12 +8,12 @@ module public import Mathlib.Algebra.Category.ModuleCat.AB public import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf public import Mathlib.Condensed.Light.Epi -/-! +/-! # Grothendieck's AB axioms for light condensed modules The category of light condensed `R`-modules over a ring satisfies the countable version of -Grothendieck's AB4* axiom +Grothendieck's AB4\* axiom -/ @[expose] public section diff --git a/Mathlib/Control/Monad/Basic.lean b/Mathlib/Control/Monad/Basic.lean index 89b1b9136d689b..8e949ddfffc1bb 100644 --- a/Mathlib/Control/Monad/Basic.lean +++ b/Mathlib/Control/Monad/Basic.lean @@ -15,9 +15,9 @@ import Mathlib.Tactic.Attr.Register ## Attributes -* ext -* functor_norm -* monad_norm +* `ext` +* `functor_norm` +* `monad_norm` ## Implementation Details diff --git a/Mathlib/Data/Complex/Basic.lean b/Mathlib/Data/Complex/Basic.lean index 13bf4285b83450..ae96276af33874 100644 --- a/Mathlib/Data/Complex/Basic.lean +++ b/Mathlib/Data/Complex/Basic.lean @@ -761,7 +761,7 @@ theorem im_eq_sub_conj (z : ℂ) : (z.im : ℂ) = (z - conj z) / (2 * I) := by simp only [sub_conj, ofReal_mul, ofReal_ofNat, mul_right_comm, mul_div_cancel_left₀ _ (mul_ne_zero two_ne_zero I_ne_zero : 2 * I ≠ 0)] -/-- Show the imaginary number ⟨x, y⟩ as an "x + y*I" string +/-- Show the imaginary number ⟨x, y⟩ as an `"x + y*I"` string Note that the Real numbers used for x and y will show as Cauchy sequences due to the way Real numbers are represented. diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/Mathlib/Data/Fin/Tuple/Basic.lean index 1cff8b57c3bfda..f83904d503e3aa 100644 --- a/Mathlib/Data/Fin/Tuple/Basic.lean +++ b/Mathlib/Data/Fin/Tuple/Basic.lean @@ -789,8 +789,8 @@ lemma forall_iff_castSucc {P : Fin (n + 1) → Prop} : (∀ i, P i) ↔ P (last n) ∧ ∀ i : Fin n, P i.castSucc := ⟨fun h ↦ ⟨h _, fun _ ↦ h _⟩, fun h ↦ lastCases h.1 h.2⟩ -/-- A finite sequence of properties P holds for {0, ..., m + n - 1} iff -it holds separately for both {0, ..., m - 1} and {m, ..., m + n - 1}. -/ +/-- A finite sequence of properties `P` holds for `{0, ..., m + n - 1}` iff +it holds separately for both `{0, ..., m - 1}` and `{m, ..., m + n - 1}`. -/ theorem forall_fin_add {m n} (P : Fin (m + n) → Prop) : (∀ i, P i) ↔ (∀ i, P (castAdd _ i)) ∧ (∀ j, P (natAdd _ j)) := ⟨fun h => ⟨fun _ => h _, fun _ => h _⟩, fun ⟨hm, hn⟩ => Fin.addCases hm hn⟩ diff --git a/Mathlib/Data/NNReal/Star.lean b/Mathlib/Data/NNReal/Star.lean index 0296293e28a6d4..2bda78221d0bd4 100644 --- a/Mathlib/Data/NNReal/Star.lean +++ b/Mathlib/Data/NNReal/Star.lean @@ -9,7 +9,7 @@ public import Mathlib.Data.NNReal.Defs public import Mathlib.Data.Real.Star /-! -# The non-negative real numbers are a `*`-ring, with the trivial `*`-structure +# The non-negative real numbers are a \*-ring, with the trivial \*-structure -/ @[expose] public section diff --git a/Mathlib/Data/Real/Basic.lean b/Mathlib/Data/Real/Basic.lean index 9b462066ead4a4..0962408a023fe2 100644 --- a/Mathlib/Data/Real/Basic.lean +++ b/Mathlib/Data/Real/Basic.lean @@ -21,7 +21,7 @@ and a conditionally complete linear order, have been deferred to the file `Mathlib/Data/Real/Archimedean.lean`, in order to keep the imports here simple. -The fact that the real numbers are a (trivial) *-ring has similarly been deferred to +The fact that the real numbers are a (trivial) \*-ring has similarly been deferred to `Mathlib/Data/Real/Star.lean`. -/ diff --git a/Mathlib/Data/Real/Star.lean b/Mathlib/Data/Real/Star.lean index e36077f7c171b1..8ba287ec24a43f 100644 --- a/Mathlib/Data/Real/Star.lean +++ b/Mathlib/Data/Real/Star.lean @@ -9,12 +9,12 @@ public import Mathlib.Algebra.Star.Basic public import Mathlib.Data.Real.Basic /-! -# The real numbers are a `*`-ring, with the trivial `*`-structure +# The real numbers are a \*-ring, with the trivial \*-structure -/ @[expose] public section -/-- The real numbers are a `*`-ring, with the trivial `*`-structure. -/ +/-- The real numbers are a \*-ring, with the trivial \*-structure. -/ instance : StarRing ℝ := starRingOfComm diff --git a/Mathlib/Data/Real/StarOrdered.lean b/Mathlib/Data/Real/StarOrdered.lean index 2e3c3f2a2a8238..31684afbb997d2 100644 --- a/Mathlib/Data/Real/StarOrdered.lean +++ b/Mathlib/Data/Real/StarOrdered.lean @@ -9,7 +9,7 @@ public import Mathlib.Algebra.Order.Star.Basic public import Mathlib.Data.NNReal.Star public import Mathlib.Data.Real.Sqrt -/-! # `ℝ` and `ℝ≥0` are *-ordered rings. -/ +/-! # `ℝ` and `ℝ≥0` are \*-ordered rings. -/ @[expose] public section diff --git a/Mathlib/Data/Set/UnionLift.lean b/Mathlib/Data/Set/UnionLift.lean index 30fdd5ad57413a..d4087289b6a21b 100644 --- a/Mathlib/Data/Set/UnionLift.lean +++ b/Mathlib/Data/Set/UnionLift.lean @@ -29,9 +29,9 @@ There are also three lemmas about `iUnionLift` intended to aid with proving that homomorphism when defined on a Union of substructures. There is one lemma each to show that constants, unary functions, or binary functions are preserved. These lemmas are: -*`Set.iUnionLift_const` -*`Set.iUnionLift_unary` -*`Set.iUnionLift_binary` +* `Set.iUnionLift_const` +* `Set.iUnionLift_unary` +* `Set.iUnionLift_binary` ## Tags diff --git a/Mathlib/FieldTheory/Fixed.lean b/Mathlib/FieldTheory/Fixed.lean index 3e94922eac74a6..97a75276b87776 100644 --- a/Mathlib/FieldTheory/Fixed.lean +++ b/Mathlib/FieldTheory/Fixed.lean @@ -20,16 +20,15 @@ public import Mathlib.RingTheory.Polynomial.Subring This is the basis of the Fundamental Theorem of Galois Theory. Given a (finite) group `G` that acts on a field `F`, we define `FixedPoints.subfield G F`, -the subfield consisting of elements of `F` fixed_points by every element of `G`. +the subfield consisting of elements of `F` fixed by every element of `G`. This subfield is then normal and separable, and in addition if `G` acts faithfully on `F` then `finrank (FixedPoints.subfield G F) F = Fintype.card G`. ## Main Definitions -- `FixedPoints.subfield G F`, the subfield consisting of elements of `F` fixed_points by every +- `FixedPoints.subfield G F`, the subfield consisting of elements of `F` fixed by every element of `G`, where `G` is a group that acts on `F`. - -/ @[expose] public section diff --git a/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean b/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean index 36d477c4f544a1..0ecf4a6ef50a94 100644 --- a/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean +++ b/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean @@ -136,7 +136,7 @@ end PartialDiffeomorph variable {M N} -/-- `f : M → N` is called a **`C^n` local diffeomorphism at *x*** iff there exist +/-- `f : M → N` is called a **`C^n` local diffeomorphism at `x`** iff there exist open sets `U ∋ x` and `V ∋ f x` and a diffeomorphism `Φ : U → V` such that `f = Φ` on `U`. -/ def IsLocalDiffeomorphAt (f : M → N) (x : M) : Prop := ∃ Φ : PartialDiffeomorph I J M N n, x ∈ Φ.source ∧ EqOn f Φ Φ.source @@ -223,7 +223,7 @@ lemma localInverse_mdifferentiableAt (hf : IsLocalDiffeomorphAt I J n f x) (hn : end IsLocalDiffeomorphAt -/-- `f : M → N` is called a **`C^n` local diffeomorphism on *s*** iff it is a local diffeomorphism +/-- `f : M → N` is called a **`C^n` local diffeomorphism on `s`** iff it is a local diffeomorphism at each `x : s`. -/ @[expose] def IsLocalDiffeomorphOn (f : M → N) (s : Set M) : Prop := ∀ x : s, IsLocalDiffeomorphAt I J n f x diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean index 8147a625735678..8799a8dd9abfb9 100644 --- a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean +++ b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean @@ -20,9 +20,9 @@ Abbreviations are also provided for `SheafedSpace`, `LocallyRingedSpace` and `Sc ## Main definitions * `AlgebraicGeometry.PresheafedSpace.IsOpenImmersion`: the `Prop`-valued typeclass asserting - that a PresheafedSpace hom `f` is an open_immersion. + that a PresheafedSpace hom `f` is an open immersion. * `AlgebraicGeometry.IsOpenImmersion`: the `Prop`-valued typeclass asserting - that a Scheme morphism `f` is an open_immersion. + that a Scheme morphism `f` is an open immersion. * `AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict`: The source of an open immersion is isomorphic to the restriction of the target onto the image. * `AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift`: Any morphism whose range is diff --git a/Mathlib/GroupTheory/Descent.lean b/Mathlib/GroupTheory/Descent.lean index 1ecc7b6fe36b72..2f79f754b19015 100644 --- a/Mathlib/GroupTheory/Descent.lean +++ b/Mathlib/GroupTheory/Descent.lean @@ -41,7 +41,7 @@ See `CommGroup.fg_of_descent` / `AddCommGroup.fg_of_descent` and This last version is one of the main ingredients of the standard proof of the **Mordell-Weil Theorem**. It allows to reduce the statement to showing that `G / 2 • G` is finite -(where `G` is the Mordell-Weil group`). +(where `G` is the Mordell-Weil group). ### Implementation note diff --git a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean index e4d92fed7ee01d..572de576b532ba 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean @@ -44,9 +44,8 @@ section AffineIndependent variable (k : Type*) {V : Type*} {P : Type*} [Ring k] [AddCommGroup V] [Module k V] variable [AffineSpace V P] {ι : Type*} -/-- An indexed family is said to be affinely independent if no -nontrivial weighted subtractions (where the sum of weights is 0) are -0. -/ +/-- An indexed family is said to be affinely independent if no nontrivial weighted subtractions +(where the sum of weights is 0) are 0. -/ def AffineIndependent (p : ι → P) : Prop := ∀ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 → s.weightedVSub p w = (0 : V) → ∀ i ∈ s, w i = 0 diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean index 02f974fff1ba33..e32f7ce158460e 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean @@ -13,7 +13,7 @@ public import Mathlib.LinearAlgebra.Dual.Defs /-! # Contraction in Clifford Algebras -This file contains some of the results from [grinberg_clifford_2016][]. +This file contains some of the results from [grinberg_clifford_2016]. The key result is `CliffordAlgebra.equivExterior`. ## Main definitions @@ -27,13 +27,13 @@ The key result is `CliffordAlgebra.equivExterior`. ## Implementation notes -This file somewhat follows [grinberg_clifford_2016][], although we are missing some of the induction +This file somewhat follows [grinberg_clifford_2016], although we are missing some of the induction principles needed to prove many of the results. Here, we avoid the quotient-based approach described -in [grinberg_clifford_2016][], instead directly constructing our objects using the universal +in [grinberg_clifford_2016], instead directly constructing our objects using the universal property. -Note that [grinberg_clifford_2016][] concludes that its contents are not novel, and are in fact just -a rehash of parts of [bourbaki2007][]; we should at some point consider swapping our references to +Note that [grinberg_clifford_2016] concludes that its contents are not novel, and are in fact just +a rehash of parts of [bourbaki2007]; we should at some point consider swapping our references to refer to the latter. Within this file, we use the local notation @@ -79,7 +79,7 @@ variable {Q} Note that $v ⌋ x$ is spelt `contractLeft (Q.associated v) x`. -This includes [grinberg_clifford_2016][] Theorem 10.75 -/ +This includes [grinberg_clifford_2016] Theorem 10.75 -/ def contractLeft : Module.Dual R M →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q where toFun d := foldr' Q (contractLeftAux Q d) (contractLeftAux_contractLeftAux Q d) 0 map_add' d₁ d₂ := @@ -108,7 +108,7 @@ right. Note that $x ⌊ v$ is spelt `contractRight x (Q.associated v)`. -This includes [grinberg_clifford_2016][] Theorem 16.75 -/ +This includes [grinberg_clifford_2016] Theorem 16.75 -/ def contractRight : CliffordAlgebra Q →ₗ[R] Module.Dual R M →ₗ[R] CliffordAlgebra Q := LinearMap.flip (LinearMap.compl₂ (LinearMap.compr₂ contractLeft reverse) reverse) @@ -120,14 +120,14 @@ local infixl:70 "⌋" => contractLeft (R := R) (M := M) local infixl:70 "⌊" => contractRight (R := R) (M := M) (Q := Q) -/-- This is [grinberg_clifford_2016][] Theorem 6 -/ +/-- This is [grinberg_clifford_2016] Theorem 6 -/ theorem contractLeft_ι_mul (a : M) (b : CliffordAlgebra Q) : d⌋(ι Q a * b) = d a • b - ι Q a * (d⌋b) := by -- Porting note: Lean cannot figure out anymore the third argument refine foldr'_ι_mul _ _ ?_ _ _ _ exact fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx -/-- This is [grinberg_clifford_2016][] Theorem 12 -/ +/-- This is [grinberg_clifford_2016] Theorem 12 -/ theorem contractRight_mul_ι (a : M) (b : CliffordAlgebra Q) : b * ι Q a⌊d = d a • b - b⌊d * ι Q a := by rw [contractRight_eq, reverse.map_mul, reverse_ι, contractLeft_ι_mul, map_sub, map_smul, @@ -183,7 +183,7 @@ theorem contractRight_one : (1 : CliffordAlgebra Q)⌊d = 0 := by variable {Q} -/-- This is [grinberg_clifford_2016][] Theorem 7 -/ +/-- This is [grinberg_clifford_2016] Theorem 7 -/ theorem contractLeft_contractLeft (x : CliffordAlgebra Q) : d⌋(d⌋x) = 0 := by induction x using CliffordAlgebra.left_induction with | algebraMap => simp_rw [contractLeft_algebraMap, map_zero] @@ -191,11 +191,11 @@ theorem contractLeft_contractLeft (x : CliffordAlgebra Q) : d⌋(d⌋x) = 0 := b | ι_mul _ _ hx => rw [contractLeft_ι_mul, map_sub, contractLeft_ι_mul, hx, map_smul, mul_zero, sub_zero, sub_self] -/-- This is [grinberg_clifford_2016][] Theorem 13 -/ +/-- This is [grinberg_clifford_2016] Theorem 13 -/ theorem contractRight_contractRight (x : CliffordAlgebra Q) : x⌊d⌊d = 0 := by rw [contractRight_eq, contractRight_eq, reverse_reverse, contractLeft_contractLeft, map_zero] -/-- This is [grinberg_clifford_2016][] Theorem 8 -/ +/-- This is [grinberg_clifford_2016] Theorem 8 -/ theorem contractLeft_comm (x : CliffordAlgebra Q) : d⌋(d'⌋x) = -(d'⌋(d⌋x)) := by induction x using CliffordAlgebra.left_induction with | algebraMap => simp_rw [contractLeft_algebraMap, map_zero, neg_zero] @@ -204,7 +204,7 @@ theorem contractLeft_comm (x : CliffordAlgebra Q) : d⌋(d'⌋x) = -(d'⌋(d⌋x simp only [contractLeft_ι_mul, map_sub, map_smul] rw [neg_sub, sub_sub_eq_add_sub, hx, mul_neg, ← sub_eq_add_neg] -/-- This is [grinberg_clifford_2016][] Theorem 14 -/ +/-- This is [grinberg_clifford_2016] Theorem 14 -/ theorem contractRight_comm (x : CliffordAlgebra Q) : x⌊d⌊d' = -(x⌊d'⌊d) := by rw [contractRight_eq, contractRight_eq, contractRight_eq, contractRight_eq, reverse_reverse, reverse_reverse, contractLeft_comm, map_neg] @@ -236,7 +236,7 @@ variable {Q' Q'' : QuadraticForm R M} {B B' : BilinForm R M} /-- Convert between two algebras of different quadratic forms, sending vectors to vectors, scalars to scalars, and adjusting products by a contraction term. -This is $\lambda_B$ from [bourbaki2007][] §9 Lemma 2. -/ +This is $\lambda_B$ from [bourbaki2007] §9 Lemma 2. -/ def changeForm (h : B.toQuadraticMap = Q' - Q) : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q' := foldr Q (changeFormAux Q' B) (fun m x => @@ -286,7 +286,7 @@ theorem changeForm_ι_mul_ι (m₁ m₂ : M) : changeForm h (ι Q m₁ * ι Q m₂) = ι Q' m₁ * ι Q' m₂ - algebraMap _ _ (B m₁ m₂) := by rw [changeForm_ι_mul, changeForm_ι, contractLeft_ι] -/-- Theorem 23 of [grinberg_clifford_2016][] -/ +/-- Theorem 23 of [grinberg_clifford_2016] -/ theorem changeForm_contractLeft (d : Module.Dual R M) (x : CliffordAlgebra Q) : changeForm h (d⌋x) = d⌋(changeForm h x) := by induction x using CliffordAlgebra.left_induction with @@ -309,7 +309,7 @@ theorem changeForm_self : changeForm changeForm.zero_proof = (LinearMap.id : CliffordAlgebra Q →ₗ[R] _) := LinearMap.ext <| changeForm_self_apply -/-- This is [bourbaki2007][] §9 Lemma 3. -/ +/-- This is [bourbaki2007] §9 Lemma 3. -/ theorem changeForm_changeForm (x : CliffordAlgebra Q) : changeForm h' (changeForm h x) = changeForm (changeForm.add_proof h h') x := by induction x using CliffordAlgebra.left_induction with @@ -325,7 +325,7 @@ theorem changeForm_comp_changeForm : /-- Any two algebras whose quadratic forms differ by a bilinear form are isomorphic as modules. -This is $\bar \lambda_B$ from [bourbaki2007][] §9 Proposition 3. -/ +This is $\bar \lambda_B$ from [bourbaki2007] §9 Proposition 3. -/ @[simps apply] def changeFormEquiv : CliffordAlgebra Q ≃ₗ[R] CliffordAlgebra Q' := { changeForm h with diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean index f1be2f3ca128af..7a89455eb57e99 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean @@ -28,7 +28,7 @@ In this file we define `lipschitzGroup`, `pinGroup` and `spinGroup` and show the The definition of the Lipschitz group $\{ x \in \mathop{\mathcal{C}\ell} | x \text{ is invertible and } x v x^{-1} ∈ V \}$ is given by: -* [fulton2004][], Chapter 20 +* [fulton2004], Chapter 20 * https://en.wikipedia.org/wiki/Clifford_algebra#Lipschitz_group But they presumably form a group only in finite dimensions. So we define `lipschitzGroup` with diff --git a/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean b/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean index 55b9eff6e462d3..27f3177c9eb8d2 100644 --- a/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean +++ b/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean @@ -116,7 +116,7 @@ theorem exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card [Finite end -/-- In a vector space with dimension 1, each set {v} is a basis for `v ≠ 0`. -/ +/-- In a vector space with dimension 1, each set `{v}` is a basis for `v ≠ 0`. -/ @[simps repr_apply] noncomputable def basisSingleton (ι : Type*) [Unique ι] (h : finrank K V = 1) (v : V) (hv : v ≠ 0) : Basis ι K V := diff --git a/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean b/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean index e802198a5800c1..865be47299d912 100644 --- a/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean +++ b/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean @@ -438,7 +438,7 @@ section variable (R) /-- Pick some representation of `x : span R w` as a linear combination in `w`, - ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose +`((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose` -/ irreducible_def Span.repr (w : Set M) (x : span R w) : w →₀ R := ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose diff --git a/Mathlib/LinearAlgebra/Matrix/ConjTranspose.lean b/Mathlib/LinearAlgebra/Matrix/ConjTranspose.lean index 077f6d5b221849..5c730990d2ca34 100644 --- a/Mathlib/LinearAlgebra/Matrix/ConjTranspose.lean +++ b/Mathlib/LinearAlgebra/Matrix/ConjTranspose.lean @@ -416,14 +416,14 @@ theorem star_apply [Star α] (M : Matrix n n α) (i j) : (star M) i j = star (M instance [InvolutiveStar α] : InvolutiveStar (Matrix n n α) where star_involutive := conjTranspose_conjTranspose -/-- When `α` is a `*`-additive monoid, `Matrix.star` is also a `*`-additive monoid. -/ +/-- When `α` is a \*-additive monoid, `Matrix.star` is also a \*-additive monoid. -/ instance [AddMonoid α] [StarAddMonoid α] : StarAddMonoid (Matrix n n α) where star_add := conjTranspose_add instance [Star α] [Star β] [SMul α β] [StarModule α β] : StarModule α (Matrix n n β) where star_smul := conjTranspose_smul -/-- When `α` is a `*`-(semi)ring, `Matrix.star` is also a `*`-(semi)ring. -/ +/-- When `α` is a \*-(semi)ring, `Matrix.star` is also a \*-(semi)ring. -/ instance [Fintype n] [NonUnitalSemiring α] [StarRing α] : StarRing (Matrix n n α) where star_add := conjTranspose_add star_mul := conjTranspose_mul diff --git a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Basic.lean b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Basic.lean index 05258c5cdd1716..bf067150aa6f5e 100644 --- a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Basic.lean +++ b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Basic.lean @@ -20,7 +20,7 @@ namespace Matrix section Examples -/-- The matrix [a, -b; b, a] (inspired by multiplication by a complex number); it is an element of +/-- The matrix $[a, -b; b, a]$ (inspired by multiplication by a complex number); it is an element of $GL_2(R)$ if `a ^ 2 + b ^ 2` is nonzero. -/ @[simps! -fullyApplied val] def planeConformalMatrix {R} [Field R] (a b : R) (hab : a ^ 2 + b ^ 2 ≠ 0) : diff --git a/Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean b/Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean index b3a27986f13106..a9282df0563c9a 100644 --- a/Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean @@ -77,8 +77,8 @@ is not a `MultilinearMap`. While this can be generalized to work for dependent `Π i : ι₁, N'₁ i` instead of `ι₁ → N`, doing so introduces `Sum.elim N'₁ N'₂` types in the result which are difficult to work with and not defeq -to the simple case defined here. See [this zulip thread]( -https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Instances.20on.20.60sum.2Eelim.20A.20B.20i.60/near/218484619). +to the simple case defined here. See +[this zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Instances.20on.20.60sum.2Eelim.20A.20B.20i.60/near/218484619). -/ @[simps! apply] def domCoprod (a : MultilinearMap R (fun _ : ι₁ => N) N₁) diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean index f75a18b6d6b858..187ca29ea3c5dc 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean @@ -16,7 +16,7 @@ public import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic ## Main statements -* `borel_eq_generateFrom_Ixx` (where Ixx is one of {Iio, Ioi, Iic, Ici, Ico, Ioc}): +* `borel_eq_generateFrom_Ixx` (where Ixx is one of `{Iio, Ioi, Iic, Ici, Ico, Ioc}`): The Borel sigma algebra of a linear order topology is generated by intervals of the given kind. * `Dense.borel_eq_generateFrom_Ico_mem`, `Dense.borel_eq_generateFrom_Ioc_mem`: The Borel sigma algebra of a dense linear order topology is generated by intervals of a given diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean index d589bd06fe92b3..c3fcf292ce6fd8 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean @@ -15,9 +15,9 @@ public import Mathlib.Topology.Instances.Real.Lemmas ## Main statements -* `borel_eq_generateFrom_Ixx_rat` (where Ixx is one of {Ioo, Ioi, Iio, Ici, Iic}): +* `borel_eq_generateFrom_Ixx_rat` (where Ixx is one of `{Ioo, Ioi, Iio, Ici, Iic}`): the Borel sigma algebra on ℝ is generated by intervals with rational endpoints; -* `isPiSystem_Ixx_rat` (where Ixx is one of {Ioo, Ioi, Iio, Ici, Iic}): +* `isPiSystem_Ixx_rat` (where Ixx is one of `{Ioo, Ioi, Iio, Ici, Iic}`): intervals with rational endpoints form a pi system on ℝ; * `measurable_real_toNNReal`, `measurable_coe_nnreal_real`, `measurable_coe_nnreal_ennreal`, `ENNReal.measurable_ofReal`, `ENNReal.measurable_toReal`: diff --git a/Mathlib/MeasureTheory/Function/Intersectivity.lean b/Mathlib/MeasureTheory/Function/Intersectivity.lean index ffdcc9cd5bc778..3175a88aca9a61 100644 --- a/Mathlib/MeasureTheory/Function/Intersectivity.lean +++ b/Mathlib/MeasureTheory/Function/Intersectivity.lean @@ -19,7 +19,7 @@ This is in some sense a finitary version of the second Borel-Cantelli lemma. ## References [Bergelson, *Sets of recurrence of `ℤᵐ`-actions and properties of sets of differences in -`ℤᵐ`][bergelson1985] +`ℤᵐ`*][bergelson1985] ## TODO diff --git a/Mathlib/MeasureTheory/Integral/Layercake.lean b/Mathlib/MeasureTheory/Integral/Layercake.lean index cd6ddd00faf986..ba4b7c4ec100fb 100644 --- a/Mathlib/MeasureTheory/Integral/Layercake.lean +++ b/Mathlib/MeasureTheory/Integral/Layercake.lean @@ -27,26 +27,26 @@ The essence of the (mathematical) proof is Fubini's theorem. We also give the most common application of the layer cake formula - a representation of the integral of a nonnegative function f: -∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) ≥ t} dt +$$∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) ≥ t} dt$$ -Variants of the formulas with measures of sets of the form {ω | f(ω) > t} instead of {ω | f(ω) ≥ t} -are also included. +Variants of the formulas with measures of sets of the form `{ω | f(ω) > t}` instead of +`{ω | f(ω) ≥ t}` are also included. ## Main results * `MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul` and `MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul`: The general layer cake formulas with Lebesgue integrals, written in terms of measures of - sets of the forms {ω | t ≤ f(ω)} and {ω | t < f(ω)}, respectively. + sets of the forms `{ω | t ≤ f(ω)}` and `{ω | t < f(ω)}`, respectively. * `MeasureTheory.lintegral_eq_lintegral_meas_le` and `MeasureTheory.lintegral_eq_lintegral_meas_lt`: The most common special cases of the layer cake formulas, stating that for a nonnegative - function f we have ∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) ≥ t} dt and - ∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) > t} dt, respectively. + function f we have $∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) ≥ t} dt$ and + $∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) > t} dt$, respectively. * `Integrable.integral_eq_integral_meas_lt`: A Bochner integral version of the most common special case of the layer cake formulas, stating that for an integrable and a.e.-nonnegative function f we have - ∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) > t} dt. + $∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) > t} dt$. ## See also diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean index 8040779246a4a4..3a177d3ffc4578 100644 --- a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean @@ -501,7 +501,7 @@ theorem toWeakDualBCNN_apply (μ : FiniteMeasure Ω) (f : Ω →ᵇ ℝ≥0) : μ.toWeakDualBCNN f = (∫⁻ x, f x ∂(μ : Measure Ω)).toNNReal := rfl /-- The topology of weak convergence on `MeasureTheory.FiniteMeasure Ω` is inherited (induced) -from the weak-* topology on `WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)` via the function +from the weak-\* topology on `WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)` via the function `MeasureTheory.FiniteMeasure.toWeakDualBCNN`. -/ instance instTopologicalSpace : TopologicalSpace (FiniteMeasure Ω) := TopologicalSpace.induced toWeakDualBCNN inferInstance diff --git a/Mathlib/ModelTheory/Algebra/Ring/Basic.lean b/Mathlib/ModelTheory/Algebra/Ring/Basic.lean index 343f4032178407..cc331daf88752e 100644 --- a/Mathlib/ModelTheory/Algebra/Ring/Basic.lean +++ b/Mathlib/ModelTheory/Algebra/Ring/Basic.lean @@ -47,7 +47,7 @@ variable {α : Type*} namespace FirstOrder /-- The type of Ring functions, to be used in the definition of the language of rings. -It contains the operations (+,*,-,0,1) -/ +It contains the operations `(+,*,-,0,1)` -/ inductive ringFunc : ℕ → Type | add : ringFunc 2 | mul : ringFunc 2 @@ -56,7 +56,7 @@ inductive ringFunc : ℕ → Type | one : ringFunc 0 deriving DecidableEq -/-- The language of rings contains the operations (+,*,-,0,1) -/ +/-- The language of rings contains the operations `(+,*,-,0,1)` -/ def Language.ring : Language := { Functions := ringFunc Relations := fun _ => Empty } diff --git a/Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean b/Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean index 243d903453ad03..3e2b29a5a921d5 100644 --- a/Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean +++ b/Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean @@ -31,8 +31,8 @@ definable. ## References * [Seymour Ginsburg and Edwin H. Spanier, *Bounded ALGOL-Like Languages*][ginsburg1964] -* [Seymour Ginsburg and Edwin H. Spanier, *Semigroups, Presburger Formulas, and Languages*][ - ginsburg1966] +* [Seymour Ginsburg and Edwin H. Spanier, *Semigroups, Presburger Formulas, and + Languages*][ginsburg1966] * [Samuel Eilenberg and M. P. Schützenberger, *Rational Sets in Commutative Monoids*][eilenberg1969] -/ diff --git a/Mathlib/ModelTheory/LanguageMap.lean b/Mathlib/ModelTheory/LanguageMap.lean index 7f639121e24cb0..a209abb76b2ac6 100644 --- a/Mathlib/ModelTheory/LanguageMap.lean +++ b/Mathlib/ModelTheory/LanguageMap.lean @@ -26,8 +26,8 @@ structures. ## References For the Flypitch project: -- [J. Han, F. van Doorn, *A formal proof of the independence of the continuum hypothesis*] - [flypitch_cpp] +- [J. Han, F. van Doorn, *A formal proof of the independence of the continuum + hypothesis*][flypitch_cpp] - [J. Han, F. van Doorn, *A formalization of forcing and the unprovability of the continuum hypothesis*][flypitch_itp] diff --git a/Mathlib/ModelTheory/Semantics.lean b/Mathlib/ModelTheory/Semantics.lean index f9b82a8e9ac9d3..ea9418de56f9a9 100644 --- a/Mathlib/ModelTheory/Semantics.lean +++ b/Mathlib/ModelTheory/Semantics.lean @@ -42,8 +42,8 @@ in a style inspired by the [Flypitch project](https://flypitch.github.io/). ## References For the Flypitch project: -- [J. Han, F. van Doorn, *A formal proof of the independence of the continuum hypothesis*] - [flypitch_cpp] +- [J. Han, F. van Doorn, *A formal proof of the independence of the continuum + hypothesis*][flypitch_cpp] - [J. Han, F. van Doorn, *A formalization of forcing and the unprovability of the continuum hypothesis*][flypitch_itp] -/ diff --git a/Mathlib/ModelTheory/Syntax.lean b/Mathlib/ModelTheory/Syntax.lean index d35639ddf380b5..1b7dfa56d6698b 100644 --- a/Mathlib/ModelTheory/Syntax.lean +++ b/Mathlib/ModelTheory/Syntax.lean @@ -52,8 +52,8 @@ This file defines first-order terms, formulas, sentences, and theories in a styl ## References For the Flypitch project: -- [J. Han, F. van Doorn, *A formal proof of the independence of the continuum hypothesis*] - [flypitch_cpp] +- [J. Han, F. van Doorn, *A formal proof of the independence of the continuum + hypothesis*][flypitch_cpp] - [J. Han, F. van Doorn, *A formalization of forcing and the unprovability of the continuum hypothesis*][flypitch_itp] -/ diff --git a/Mathlib/NumberTheory/MulChar/Duality.lean b/Mathlib/NumberTheory/MulChar/Duality.lean index b16320a20d07df..b9d58aef54f092 100644 --- a/Mathlib/NumberTheory/MulChar/Duality.lean +++ b/Mathlib/NumberTheory/MulChar/Duality.lean @@ -76,7 +76,7 @@ lemma card_eq_card_units_of_hasEnoughRootsOfUnity : Nat.card (MulChar M R) = Nat /-- -Let `N` be a submonoid of `M` group and let R` be a ring with enough roots of unity. +Let `N` be a submonoid of `M` group and let `R` be a ring with enough roots of unity. Then any `R`-value multiplicative character of `N` can be extended to a multiplicative character of `M`. -/ diff --git a/Mathlib/NumberTheory/Multiplicity.lean b/Mathlib/NumberTheory/Multiplicity.lean index 9f30b386de0c49..1da29afb30f9e5 100644 --- a/Mathlib/NumberTheory/Multiplicity.lean +++ b/Mathlib/NumberTheory/Multiplicity.lean @@ -22,8 +22,7 @@ This file contains results in number theory relating to multiplicity. ## References -* [Wikipedia, *Lifting-the-exponent lemma*] - (https://en.wikipedia.org/wiki/Lifting-the-exponent_lemma) +* [Wikipedia, *Lifting-the-exponent lemma*](https://en.wikipedia.org/wiki/Lifting-the-exponent_lemma) -/ public section diff --git a/Mathlib/NumberTheory/Padics/Hensel.lean b/Mathlib/NumberTheory/Padics/Hensel.lean index 9c4b4023cd42e1..c05332b90ebb10 100644 --- a/Mathlib/NumberTheory/Padics/Hensel.lean +++ b/Mathlib/NumberTheory/Padics/Hensel.lean @@ -12,9 +12,9 @@ public import Mathlib.Topology.Algebra.Polynomial public import Mathlib.Topology.MetricSpace.CauSeqFilter /-! -# Hensel's lemma on ℤ_p +# Hensel's lemma on `ℤ_p` -This file proves Hensel's lemma on ℤ_p, roughly following Keith Conrad's writeup: +This file proves Hensel's lemma on `ℤ_p`, roughly following Keith Conrad's writeup: Hensel's lemma gives a simple condition for the existence of a root of a polynomial. diff --git a/Mathlib/NumberTheory/Padics/PadicNorm.lean b/Mathlib/NumberTheory/Padics/PadicNorm.lean index 1da53df08a88fe..69de4c02ec2c4c 100644 --- a/Mathlib/NumberTheory/Padics/PadicNorm.lean +++ b/Mathlib/NumberTheory/Padics/PadicNorm.lean @@ -18,7 +18,7 @@ denominator of `q`. This function obeys the standard properties of a valuation, assumptions on `p`. The valuation induces a norm on `ℚ`. This norm is a nonarchimedean absolute value. -It takes values in {0} ∪ {1/p^k | k ∈ ℤ}. +It takes values in `{0} ∪ {1/p^k | k ∈ ℤ}`. ## Implementation notes diff --git a/Mathlib/Order/ModularLattice.lean b/Mathlib/Order/ModularLattice.lean index 1334ac499ce409..4702db1d0bd2d3 100644 --- a/Mathlib/Order/ModularLattice.lean +++ b/Mathlib/Order/ModularLattice.lean @@ -46,8 +46,8 @@ We define (semi)modularity typeclasses as Prop-valued mixins. ## References -* [Manfred Stern, *Semimodular lattices. {Theory} and applications*][stern2009] -* [Wikipedia, *Modular Lattice*][https://en.wikipedia.org/wiki/Modular_lattice] +* [Manfred Stern, *Semimodular lattices. Theory and applications*][stern2009] +* [Wikipedia, Modular Lattice](https://en.wikipedia.org/wiki/Modular_lattice) ## TODO diff --git a/Mathlib/RingTheory/Ideal/NatInt.lean b/Mathlib/RingTheory/Ideal/NatInt.lean index 813fc7da012cba..71f82418f857da 100644 --- a/Mathlib/RingTheory/Ideal/NatInt.lean +++ b/Mathlib/RingTheory/Ideal/NatInt.lean @@ -18,7 +18,7 @@ public import Mathlib.RingTheory.PrincipalIdealDomain ## Main results -* `Ideal.isPrime_nat_iff`: the prime ideals in ℕ are ⟨0⟩, ⟨p⟩ (for prime `p`), and ⟨2, 3⟩ = {1}ᶜ. +* `Ideal.isPrime_nat_iff`: the prime ideals in ℕ are ⟨0⟩, ⟨p⟩ (for prime `p`), and `⟨2, 3⟩ = {1}ᶜ`. The proof follows https://math.stackexchange.com/a/4224486. * `Ideal.isPrime_int_iff` : the prime ideals in ℤ are ⟨0⟩ and ⟨p⟩ (for prime `p`). diff --git a/Mathlib/RingTheory/IdealFilter/Basic.lean b/Mathlib/RingTheory/IdealFilter/Basic.lean index 7676090772ef84..1a486d54795ed3 100644 --- a/Mathlib/RingTheory/IdealFilter/Basic.lean +++ b/Mathlib/RingTheory/IdealFilter/Basic.lean @@ -55,9 +55,9 @@ change the induced topology. * [Bo Stenström, *Rings and Modules of Quotients*][stenstrom1971] * [Bo Stenström, *Rings of Quotients*][stenstrom1975] -* [nLab: Uniform filter]() -* [nLab: Gabriel filter]() -* [nLab: Gabriel composition]() +* [nLab: Uniform filter](https://ncatlab.org/nlab/show/uniform+filter) +* [nLab: Gabriel filter](https://ncatlab.org/nlab/show/Gabriel+filter) +* [nLab: Gabriel composition](https://ncatlab.org/nlab/show/Gabriel+composition+of+filters) ## Tags @@ -157,7 +157,7 @@ lemma isPFilter_gabrielComposition (F G : IdealFilter A) : exact ⟨K, hK, hIK.mono_left hIJ⟩ /-- The Gabriel composition of ideal filters `F` and `G`. -See [nLab: Gabriel composition](). -/ +See [nLab: Gabriel composition](https://ncatlab.org/nlab/show/Gabriel+composition+of+filters). -/ def gabrielComposition (F G : IdealFilter A) : IdealFilter A := (isPFilter_gabrielComposition F G).toPFilter @@ -165,7 +165,7 @@ def gabrielComposition (F G : IdealFilter A) : IdealFilter A := scoped infixl:70 " • " => gabrielComposition /-- An ideal filter is Gabriel if it satisfies `IsUniform` and axiom T4. -See [nLab: Gabriel filter](). -/ +See [nLab: Gabriel filter](https://ncatlab.org/nlab/show/Gabriel+filter). -/ class IsGabriel (F : IdealFilter A) extends F.IsUniform where /-- **Axiom T4.** See [stenstrom1975]. -/ gabriel_closed (I : Ideal A) (h : ∃ J ∈ F, ∀ x ∈ J, I.colon {x} ∈ F) : I ∈ F diff --git a/Mathlib/RingTheory/IdealFilter/Topology.lean b/Mathlib/RingTheory/IdealFilter/Topology.lean index 99c3360b4a0a2c..09c597b7fe4503 100644 --- a/Mathlib/RingTheory/IdealFilter/Topology.lean +++ b/Mathlib/RingTheory/IdealFilter/Topology.lean @@ -29,7 +29,7 @@ uniform ideal filters in terms of ring filter bases. ## References -* [nLab: Uniform filter]() +* [nLab: Uniform filter](https://ncatlab.org/nlab/show/uniform+filter) ## Tags diff --git a/Mathlib/RingTheory/MvPowerSeries/Basic.lean b/Mathlib/RingTheory/MvPowerSeries/Basic.lean index b2f14228d7025b..978cb6f8e387f4 100644 --- a/Mathlib/RingTheory/MvPowerSeries/Basic.lean +++ b/Mathlib/RingTheory/MvPowerSeries/Basic.lean @@ -718,7 +718,7 @@ theorem monomial_pow (m : σ →₀ ℕ) (a : R) (n : ℕ) : /-- Vanishing of coefficients of powers of multivariate power series when the constant coefficient is nilpotent -[N. Bourbaki, *Algebra {II}*, Chapter 4, §4, n°2, proposition 3][bourbaki1981] -/ +[N. Bourbaki, *Algebra II*, Chapter 4, §4, n°2, proposition 3][bourbaki1981] -/ theorem coeff_eq_zero_of_constantCoeff_nilpotent {f : MvPowerSeries σ R} {m : ℕ} (hf : constantCoeff f ^ m = 0) {d : σ →₀ ℕ} {n : ℕ} (hn : m + degree d ≤ n) : coeff d (f ^ n) = 0 := by diff --git a/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean b/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean index 0672dcc87d9d6b..13af1ae4ed3cc1 100644 --- a/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean +++ b/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean @@ -28,7 +28,7 @@ When `R` has `UniformSpace R`, we define the corresponding uniform structure. This topology can be included by writing `open scoped MvPowerSeries.WithPiTopology`. When the type of coefficients has the discrete topology, it corresponds to the topology defined by -[N. Bourbaki, *Algebra {II}*, Chapter 4, §4, n°2][bourbaki1981]. +[N. Bourbaki, *Algebra II*, Chapter 4, §4, n°2][bourbaki1981]. It is *not* the adic topology in general. @@ -227,7 +227,7 @@ theorem isTopologicallyNilpotent_of_constantCoeff_zero [CommSemiring R] /-- Assuming the base ring has a discrete topology, the powers of a `MvPowerSeries` converge to 0 iff its constant coefficient is nilpotent. -[N. Bourbaki, *Algebra {II}*, Chapter 4, §4, n°2, corollary of prop. 3][bourbaki1981] +[N. Bourbaki, *Algebra II*, Chapter 4, §4, n°2, corollary of prop. 3][bourbaki1981] See also `MvPowerSeries.LinearTopology.isTopologicallyNilpotent_iff_constantCoeff`. -/ theorem isTopologicallyNilpotent_iff_constantCoeff_isNilpotent diff --git a/Mathlib/RingTheory/PowerSeries/PiTopology.lean b/Mathlib/RingTheory/PowerSeries/PiTopology.lean index ef0d0b8f5043e5..3ee4f3f08d4bd0 100644 --- a/Mathlib/RingTheory/PowerSeries/PiTopology.lean +++ b/Mathlib/RingTheory/PowerSeries/PiTopology.lean @@ -24,7 +24,7 @@ When `R` has `UniformSpace R`, we define the corresponding uniform structure. This topology can be included by writing `open scoped PowerSeries.WithPiTopology`. When the type of coefficients has the discrete topology, it corresponds to the topology defined by -[N. Bourbaki, *Algebra {II}*, Chapter 4, §4, n°2][bourbaki1981]. +[N. Bourbaki, *Algebra II*, Chapter 4, §4, n°2][bourbaki1981]. It corresponds with the adic topology but this is not proved here. @@ -303,7 +303,7 @@ theorem isTopologicallyNilpotent_of_constantCoeff_zero [CommSemiring R] /-- Assuming the base ring has a discrete topology, the powers of a `PowerSeries` converge to 0 iff its constant coefficient is nilpotent. -[N. Bourbaki, *Algebra {II}*, Chapter 4, §4, n°2, corollary of prop. 3][bourbaki1981] -/ +[N. Bourbaki, *Algebra II*, Chapter 4, §4, n°2, corollary of prop. 3][bourbaki1981] -/ theorem isTopologicallyNilpotent_iff_constantCoeff_isNilpotent [CommRing R] [DiscreteTopology R] (f : PowerSeries R) : Tendsto (fun n : ℕ => f ^ n) atTop (nhds 0) ↔ diff --git a/Mathlib/RingTheory/Spectrum/Prime/Topology.lean b/Mathlib/RingTheory/Spectrum/Prime/Topology.lean index 19f55b1fbd6557..e5aec7d7c6a92f 100644 --- a/Mathlib/RingTheory/Spectrum/Prime/Topology.lean +++ b/Mathlib/RingTheory/Spectrum/Prime/Topology.lean @@ -1117,7 +1117,7 @@ open TopologicalSpace (Clopens) bijection with pairs of elements with product 0 and sum 1. (By definition, `(e₁, f₁) ≤ (e₂, f₂)` iff `e₁ * e₂ = e₁`.) Both elements in such pairs must be idempotents, but there may exists idempotents that do not form such pairs (does not have a "complement"). For example, in the -semiring {0, 0.5, 1} with ⊔ as + and ⊓ as *, 0.5 has no complement. -/ +semiring `{0, 0.5, 1}` with `⊔` as `+` and `⊓` as `*`, `0.5` has no complement. -/ def mulZeroAddOneEquivClopens : {e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1} ≃o Clopens (PrimeSpectrum R) where toEquiv := .ofBijective diff --git a/Mathlib/Tactic/FieldSimp.lean b/Mathlib/Tactic/FieldSimp.lean index bd9d4b3e24780f..c1313ce98e51cb 100644 --- a/Mathlib/Tactic/FieldSimp.lean +++ b/Mathlib/Tactic/FieldSimp.lean @@ -318,7 +318,7 @@ namespace qNF /-- Extract a common factor `L` of two products-of-powers `l₁` and `l₂` in `M`, in the sense that both `l₁` and `l₂` are quotients by `L` of products of *positive* powers. -The variable `cond` specifies whether we extract a *certified nonzero[/positive]* (and therefore +The variable `cond` specifies whether we extract a *certified nonzero(/positive)* (and therefore potentially smaller) common factor. If so, the metaprogram returns a "proof" that this common factor is nonzero/positive, i.e. an expression `Q(NF.eval $(L.toNF) ≠ 0)` / `Q(0 < NF.eval $(L.toNF))`. -/ partial def gcd (iM : Q(CommGroupWithZero $M)) (l₁ l₂ : qNF M) diff --git a/Mathlib/Tactic/Ring/Basic.lean b/Mathlib/Tactic/Ring/Basic.lean index a49038ec4a8d55..6ec66234017a0c 100644 --- a/Mathlib/Tactic/Ring/Basic.lean +++ b/Mathlib/Tactic/Ring/Basic.lean @@ -465,7 +465,7 @@ partial def inv {u : Lean.Level} {α : Q(Type u)} (_sα : Q(CommSemiring $α)) return some ⟨_, vc, q($pc)⟩ | none => return none -/-- Try to evaluate an expression as a rational constant using norm_num. -/ +/-- Try to evaluate an expression as a rational constant using `norm_num`. -/ partial def derive {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring $α)) (x : Q($α)) : MetaM (Result (Common.ExSum RatCoeff sα) q($x)) := do let res ← NormNum.derive x diff --git a/Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean b/Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean index 9d4af3b6c1b098..d9d772218efd43 100644 --- a/Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean +++ b/Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean @@ -73,12 +73,12 @@ attribute [instance] ProfiniteGrp.group ProfiniteGrp.topologicalGroup /-- Construct a term of `ProfiniteGrp` from a type endowed with the structure of a compact and totally disconnected topological group. -(The condition of being Hausdorff can be omitted here because totally disconnected implies that {1} -is a closed set, thus implying Hausdorff in a topological group.) -/ +(The condition of being Hausdorff can be omitted here because totally disconnected implies that +`{1}` is a closed set, thus implying Hausdorff in a topological group.) -/ @[to_additive /-- Construct a term of `ProfiniteAddGrp` from a type endowed with the structure of a compact and totally disconnected topological additive group. -(The condition of being Hausdorff can be omitted here because totally disconnected implies that {0} -is a closed set, thus implying Hausdorff in a topological additive group.) -/] +(The condition of being Hausdorff can be omitted here because totally disconnected implies that +`{0}` is a closed set, thus implying Hausdorff in a topological additive group.) -/] abbrev ProfiniteGrp.of (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : ProfiniteGrp.{u} where toProfinite := .of G diff --git a/Mathlib/Topology/Algebra/Module/PerfectPairing.lean b/Mathlib/Topology/Algebra/Module/PerfectPairing.lean index 81d5811fc97513..879bd305d91f77 100644 --- a/Mathlib/Topology/Algebra/Module/PerfectPairing.lean +++ b/Mathlib/Topology/Algebra/Module/PerfectPairing.lean @@ -17,7 +17,7 @@ For a topological ring `R` and two topological modules `M` and `N`, a continuous a continuous bilinear map `M × N → R` that is bijective in both arguments. We require continuity in the forward direction only so that we can put several different topologies -on the continuous dual (e.g., strong, weak, weak-*). For example, if `M` is weakly reflexive then +on the continuous dual (e.g., strong, weak, weak-\*). For example, if `M` is weakly reflexive then there is a continuous perfect pairing between `M` and `WeakDual R M`, even though the map `WeakDual R M ≃ₗ[R] StrongDual R M` (where `StrongDual R M` is equipped with its strong topology) is not in general a homeomorphism. @@ -40,7 +40,7 @@ variable {R M N : Type*} is a continuous bilinear map `M × N → R` that is bijective in both arguments. We require continuity in the forward direction only so that we can put several different topologies -on the continuous dual: strong, weak, weak-* topology... -/ +on the continuous dual: strong, weak, weak-\* topology... -/ @[ext] class IsContPerfPair (p : M →ₗ[R] N →ₗ[R] R) where continuous_uncurry (p) : Continuous fun (x, y) ↦ p x y diff --git a/Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean b/Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean index 95489510b464d0..2bb4642cf9cfbb 100644 --- a/Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean +++ b/Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean @@ -20,7 +20,7 @@ Here is a list of type aliases for `E →L[𝕜] F` endowed with various topolog * `ContinuousLinearMap`: topology of bounded convergence * `UniformConvergenceCLM`: topology of `𝔖`-convergence, for a general `𝔖 : Set (Set E)` * `CompactConvergenceCLM`: topology of compact convergence -* `PointwiseConvergenceCLM`: topology of pointwise convergence, also called "weak-* topology" +* `PointwiseConvergenceCLM`: topology of pointwise convergence, also called "weak-\* topology" or "strong-operator topology" depending on the context * `ContinuousLinearMapWOT`: topology of weak pointwise convergence, also called "weak-operator topology" diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean index 3ac14b91c5faec..30e5f846acf742 100644 --- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean +++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean @@ -23,7 +23,7 @@ Here is a list of type aliases for `E →L[𝕜] F` endowed with various topolog * `ContinuousLinearMap`: topology of bounded convergence * `UniformConvergenceCLM`: topology of `𝔖`-convergence, for a general `𝔖 : Set (Set E)` * `CompactConvergenceCLM`: topology of compact convergence -* `PointwiseConvergenceCLM`: topology of pointwise convergence, also called "weak-* topology" +* `PointwiseConvergenceCLM`: topology of pointwise convergence, also called "weak-\* topology" or "strong-operator topology" depending on the context * `ContinuousLinearMapWOT`: topology of weak pointwise convergence, also called "weak-operator topology" diff --git a/Mathlib/Topology/Algebra/Module/Spaces/PointwiseConvergenceCLM.lean b/Mathlib/Topology/Algebra/Module/Spaces/PointwiseConvergenceCLM.lean index f40275189156a6..5892373be661dd 100644 --- a/Mathlib/Topology/Algebra/Module/Spaces/PointwiseConvergenceCLM.lean +++ b/Mathlib/Topology/Algebra/Module/Spaces/PointwiseConvergenceCLM.lean @@ -56,7 +56,7 @@ variable (σ E F) in sometimes also called the *strong operator topology*. We avoid this terminology since so many other things share similar names, and using "pointwise convergence" in the name is more informative. -This topology is also known as the weak*-topology in the case that `σ = RingHom.id 𝕜` and `F = 𝕜` -/ +This topology is also known as the weak⋆-topology in the case that `σ = RingHom.id 𝕜` and `F = 𝕜` -/ abbrev PointwiseConvergenceCLM := UniformConvergenceCLM σ F {s : Set E | Finite s} @[inherit_doc] @@ -156,7 +156,7 @@ def _root_.ContinuousLinearMap.toPointwiseConvergenceCLM [ContinuousSMul 𝕜₁ (fun _ ↦ Set.Finite.isVonNBounded) variable (𝕜 E) in -/-- The topology of pointwise convergence on `E →Lₚₜ[𝕜] 𝕜` coincides with the weak-* topology. -/ +/-- The topology of pointwise convergence on `E →Lₚₜ[𝕜] 𝕜` coincides with the weak-\* topology. -/ @[simps!] def equivWeakDual : (E →Lₚₜ[𝕜] 𝕜) ≃L[𝕜] WeakDual 𝕜 E where __ := LinearEquiv.refl 𝕜 (E →L[𝕜] 𝕜) diff --git a/Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean b/Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean index 84ff1a3279c2c8..80fc8e9da06cff 100644 --- a/Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean +++ b/Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean @@ -28,7 +28,7 @@ The most important examples for such topologies are: when `𝔖` is the set of `IsVonNBounded` subsets. This coincides with the operator norm topology in the case of `NormedSpace`s, and is declared as an instance on `E →L[𝕜] F` -- the topology of pointwise convergence (also called "weak-* topology" +- the topology of pointwise convergence (also called "weak-\* topology" or "strong-operator topology" depending on the context), when `𝔖` is the set of finite sets or the set of singletons. This is declared as an instance on `PointwiseConvergenceCLM`. - the topology of compact convergence, when `𝔖` is the set of compact diff --git a/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean b/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean index 60610f7c2493c6..ae02942e1b3dc0 100644 --- a/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean +++ b/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean @@ -18,8 +18,8 @@ which defines the weak topology given two vector spaces `E` and `F` over a commu such that for all `y : F` every map `fun x => B x y` is continuous. In this file, we consider two special cases. -In the case that `F = E →L[𝕜] 𝕜` and `B` being the canonical pairing, we obtain the weak-* topology, -`WeakDual 𝕜 E := (E →L[𝕜] 𝕜)`. Interchanging the arguments in the bilinear form yields the +In the case that `F = E →L[𝕜] 𝕜` and `B` being the canonical pairing, we obtain the weak-\* +topology, `WeakDual 𝕜 E := (E →L[𝕜] 𝕜)`. Interchanging the arguments in the bilinear form yields the weak topology `WeakSpace 𝕜 E := E`. ## Main definitions @@ -29,7 +29,7 @@ with the respective topology instances on it. * `WeakDual 𝕜 E` is a type synonym for `Dual 𝕜 E` (when the latter is defined): both are equal to the type `E →L[𝕜] 𝕜` of continuous linear maps from a module `E` over `𝕜` to the ring `𝕜`. -* The instance `WeakDual.instTopologicalSpace` is the weak-* topology on `WeakDual 𝕜 E`, i.e., the +* The instance `WeakDual.instTopologicalSpace` is the weak-\* topology on `WeakDual 𝕜 E`, i.e., the coarsest topology making the evaluation maps at all `z : E` continuous. * `WeakSpace 𝕜 E` is a type synonym for `E` (when the latter is defined). * The instance `WeakSpace.instTopologicalSpace` is the weak topology on `E`, i.e., the diff --git a/Mathlib/Topology/Algebra/WithZeroTopology.lean b/Mathlib/Topology/Algebra/WithZeroTopology.lean index a74130c60c00f4..8a580e650d1098 100644 --- a/Mathlib/Topology/Algebra/WithZeroTopology.lean +++ b/Mathlib/Topology/Algebra/WithZeroTopology.lean @@ -43,7 +43,8 @@ variable {α Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] {γ γ₁ γ {f : α → Γ₀} /-- The topology on a linearly ordered commutative group with a zero element adjoined. -A subset U is open if 0 ∉ U or if there is an invertible element γ₀ such that {γ | γ < γ₀} ⊆ U. -/ +A subset `U` is open if `0 ∉ U` or if there is an invertible element γ₀ such that +`{γ | γ < γ₀} ⊆ U`. -/ scoped instance (priority := 100) topologicalSpace : TopologicalSpace Γ₀ := nhdsAdjoint 0 <| ⨅ γ ≠ 0, 𝓟 (Iio γ) diff --git a/Mathlib/Topology/Homotopy/Lifting.lean b/Mathlib/Topology/Homotopy/Lifting.lean index c201a1412841b4..a240ddcae7f491 100644 --- a/Mathlib/Topology/Homotopy/Lifting.lean +++ b/Mathlib/Topology/Homotopy/Lifting.lean @@ -354,7 +354,7 @@ theorem homotopicRel_iff_comp [PreconnectedSpace A] {f₀ f₁ : C(A, E)} {S : S (ContinuousMap.comp ⟨p, cov.continuous⟩ f₀).HomotopicRel (.comp ⟨p, cov.continuous⟩ f₁) S := ⟨fun ⟨F⟩ ↦ ⟨F.compContinuousMap _⟩, fun ⟨F⟩ ↦ ⟨cov.liftHomotopyRel F he rfl rfl⟩⟩ -/-- Lifting two paths that are homotopic relative to {0,1} +/-- Lifting two paths that are homotopic relative to `{0,1}` starting from the same point also ends up in the same point. -/ theorem liftPath_apply_one_eq_of_homotopicRel {γ₀ γ₁ : C(I, X)} (h : γ₀.HomotopicRel γ₁ {0,1}) (e : E) (h₀ : γ₀ 0 = p e) (h₁ : γ₁ 0 = p e) : diff --git a/Mathlib/Topology/Order/HullKernel.lean b/Mathlib/Topology/Order/HullKernel.lean index 6a47cc2d38d3af..4dd6f6e091bc06 100644 --- a/Mathlib/Topology/Order/HullKernel.lean +++ b/Mathlib/Topology/Order/HullKernel.lean @@ -45,7 +45,7 @@ primitive spectrum of the lattice of M-ideals of a Banach space. ## References * [Gierz et al, *A Compendium of Continuous Lattices*][GierzEtAl1980] -* [Henriksen et al, *Joincompact spaces, continuous lattices and C*-algebras*][henriksen_et_al1997] +* [Henriksen et al, *Joincompact spaces, continuous lattices and C⋆-algebras*][henriksen_et_al1997] ## Tags diff --git a/Mathlib/Topology/Sion.lean b/Mathlib/Topology/Sion.lean index 1b8b6abc3f55bd..d9abac39346f70 100644 --- a/Mathlib/Topology/Sion.lean +++ b/Mathlib/Topology/Sion.lean @@ -27,7 +27,7 @@ The classical case of the theorem assumes that `f` is continuous, As a particular case, one get the von Neumann theorem where `f` is bilinear and `E`, `F` are finite dimensional. -We follow the proof of [Komiya-1988][Komiya (1988)]. +We follow the proof of [Komiya (1988)][Komiya-1988]. ## Remark on implementation @@ -52,14 +52,14 @@ We follow the proof of [Komiya-1988][Komiya (1988)]. ## References -- [vonNeumann-1928][Neumann, John von (1928). - ”Zur Theorie der Gesellschaftsspiele”. *Mathematische Annalen* 100 (1): 295‑320] +- [Neumann, John von (1928). + ”Zur Theorie der Gesellschaftsspiele”. *Mathematische Annalen* 100 (1): 295‑320][vonNeumann-1928] -- [Sion-1958][Sion, Maurice (1958). - ”On general minimax theorems”. *Pacific Journal of Mathematics* 8 (1): 171‑76.] +- [Sion, Maurice (1958). + ”On general minimax theorems”. *Pacific Journal of Mathematics* 8 (1): 171‑76.][Sion-1958] -- [Komiya-1988][Komiya, Hidetoshi (1988). - “Elementary Proof for Sion’s Minimax Theorem”. *Kodai Mathematical Journal* 11 (1).] +- [Komiya, Hidetoshi (1988). + “Elementary Proof for Sion’s Minimax Theorem”. *Kodai Mathematical Journal* 11 (1).][Komiya-1988] -/ diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean index 153b4259a1b1ed..dc707f93247aa6 100644 --- a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean +++ b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean @@ -27,7 +27,7 @@ Usual examples of the second construction include: - the topology of compact convergence, when `𝔖` is the set of compacts of `α` - the strong topology on the dual of a topological vector space (TVS) `E`, when `𝔖` is the set of Von Neumann bounded subsets of `E` -- the weak-* topology on the dual of a TVS `E`, when `𝔖` is the set of singletons of `E`. +- the weak-\* topology on the dual of a TVS `E`, when `𝔖` is the set of singletons of `E`. This file contains a lot of technical facts, so it is heavily commented, proofs included!