chore(*): small docstring syntax fixes

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

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

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 (·)) <|

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

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

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

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)
 

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

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.

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.

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

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.

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].
 -/

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

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

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

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

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

Mathlib/Algebra/Star/Subalgebra.lean

@@ -13,24 +13,24 @@ 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. -/
   star_mem' {a} : a ∈ carrier → star a ∈ carrier
 
 namespace StarSubalgebra
 
-/-- Forgetting that a *-subalgebra is closed under *.
+/-- Forgetting that a \*-subalgebra is closed under \*.
 -/
 add_decl_doc StarSubalgebra.toSubalgebra
 

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

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

Mathlib/AlgebraicGeometry/Geometrically/Irreducible.lean

@@ -15,15 +15,15 @@ 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.
 - `AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace`:
   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

Mathlib/AlgebraicGeometry/Geometrically/Reduced.lean

@@ -16,15 +16,15 @@ 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.
 - `AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian`:
   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.

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 _