doc: convert many comments into doc comments (#11940)

All of these changes appear to be oversights to me.

Mathlib/Algebra/Algebra/Basic.lean

@@ -434,7 +434,7 @@ theorem coe_linearMap : ⇑(Algebra.linearMap R A) = algebraMap R A :=
   rfl
 #align algebra.coe_linear_map Algebra.coe_linearMap
 
-/- The identity map inducing an `Algebra` structure. -/
+/-- The identity map inducing an `Algebra` structure. -/
 instance id : Algebra R R where
   -- We override `toFun` and `toSMul` because `RingHom.id` is not reducible and cannot
   -- be made so without a significant performance hit.

Mathlib/Algebra/Group/AddChar.lean

@@ -60,7 +60,7 @@ structure AddChar where
 
   Do not use this directly. Instead use `AddChar.map_zero_one`. -/
   map_zero_one' : toFun 0 = 1
-  /- The function maps addition in `A` to multiplication in `M`.
+  /-- The function maps addition in `A` to multiplication in `M`.
 
   Do not use this directly. Instead use `AddChar.map_add_mul`. -/
   map_add_mul' : ∀ a b : A, toFun (a + b) = toFun a * toFun b

Mathlib/Algebra/Group/Defs.lean

@@ -1045,7 +1045,7 @@ end InvOneClass
 `-(a + b) = -b + -a` and `a + b = 0 → -a = b`. -/
 class SubtractionMonoid (G : Type u) extends SubNegMonoid G, InvolutiveNeg G where
   protected neg_add_rev (a b : G) : -(a + b) = -b + -a
-  /- Despite the asymmetry of `neg_eq_of_add`, the symmetric version is true thanks to the
+  /-- Despite the asymmetry of `neg_eq_of_add`, the symmetric version is true thanks to the
   involutivity of negation. -/
   protected neg_eq_of_add (a b : G) : a + b = 0 → -a = b
 #align subtraction_monoid SubtractionMonoid
@@ -1057,7 +1057,7 @@ This is the immediate common ancestor of `Group` and `GroupWithZero`. -/
 @[to_additive SubtractionMonoid]
 class DivisionMonoid (G : Type u) extends DivInvMonoid G, InvolutiveInv G where
   protected mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹
-  /- Despite the asymmetry of `inv_eq_of_mul`, the symmetric version is true thanks to the
+  /-- Despite the asymmetry of `inv_eq_of_mul`, the symmetric version is true thanks to the
   involutivity of inversion. -/
   protected inv_eq_of_mul (a b : G) : a * b = 1 → a⁻¹ = b
 #align division_monoid DivisionMonoid

Mathlib/Algebra/HierarchyDesign.lean

@@ -109,7 +109,7 @@ when applicable:
   See `Mathlib.Data.Equiv.TransferInstance` for more examples. See also the `transport` tactic.
   ```
   def Equiv.Z (e : α ≃ β) [Z β] : Z α := ...
-  /- When there is a new notion of `Z`-equiv: -/
+  /-- When there is a new notion of `Z`-equiv: -/
   def Equiv.ZEquiv (e : α ≃ β) [Z β] : by { letI := Equiv.Z e, exact α ≃Z β } := ...
   ```
 

Mathlib/Algebra/Module/Pi.lean

@@ -70,8 +70,7 @@ instance module (α) {r : Semiring α} {m : ∀ i, AddCommMonoid <| f i} [∀ i,
 /- Extra instance to short-circuit type class resolution.
 For unknown reasons, this is necessary for certain inference problems. E.g., for this to succeed:
 ```lean
-example (β X : Type*) [NormedAddCommGroup β] [NormedSpace ℝ β] : Module ℝ (X → β) :=
-inferInstance
+example (β X : Type*) [NormedAddCommGroup β] [NormedSpace ℝ β] : Module ℝ (X → β) := inferInstance
 ```
 See: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclass.20resolution.20under.20binders/near/281296989
 -/

Mathlib/Algebra/Ring/Defs.lean

@@ -429,7 +429,7 @@ instance (priority := 100) Ring.toNonAssocRing : NonAssocRing α :=
   { ‹Ring α› with }
 #align ring.to_non_assoc_ring Ring.toNonAssocRing
 
-/- The instance from `Ring` to `Semiring` happens often in linear algebra, for which all the basic
+/-- The instance from `Ring` to `Semiring` happens often in linear algebra, for which all the basic
 definitions are given in terms of semirings, but many applications use rings or fields. We increase
 a little bit its priority above 100 to try it quickly, but remaining below the default 1000 so that
 more specific instances are tried first. -/

Mathlib/Analysis/Convex/Exposed.lean

@@ -100,7 +100,7 @@ protected theorem antisymm (hB : IsExposed 𝕜 A B) (hA : IsExposed 𝕜 B A) :
   hA.subset.antisymm hB.subset
 #align is_exposed.antisymm IsExposed.antisymm
 
-/- `IsExposed` is *not* transitive: Consider a (topologically) open cube with vertices
+/-! `IsExposed` is *not* transitive: Consider a (topologically) open cube with vertices
 `A₀₀₀, ..., A₁₁₁` and add to it the triangle `A₀₀₀A₀₀₁A₀₁₀`. Then `A₀₀₁A₀₁₀` is an exposed subset
 of `A₀₀₀A₀₀₁A₀₁₀` which is an exposed subset of the cube, but `A₀₀₁A₀₁₀` is not itself an exposed
 subset of the cube. -/

Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean

@@ -63,7 +63,7 @@ theorem convexOn_exp : ConvexOn ℝ univ exp :=
   strictConvexOn_exp.convexOn
 #align convex_on_exp convexOn_exp
 
-/- `Real.log` is strictly concave on $(0, +∞)$. -/
+/-- `Real.log` is strictly concave on `(0, +∞)`. -/
 theorem strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Ioi 0) log := by
   apply strictConcaveOn_of_slope_strict_anti_adjacent (convex_Ioi (0 : ℝ))
   intro x y z (hx : 0 < x) (hz : 0 < z) hxy hyz

Mathlib/Analysis/Fourier/FourierTransform.lean

@@ -118,8 +118,9 @@ end Defs
 
 section Continuous
 
-/- In this section we assume 𝕜, V, W have topologies, and L, e are continuous (but f needn't be).
-   This is used to ensure that `e [-L v w]` is (ae strongly) measurable. We could get away with
+/-! In this section we assume 𝕜, `V`, `W` have topologies,
+  and `L`, `e` are continuous (but `f` needn't be).
+   This is used to ensure that `e [-L v w]` is (a.e. strongly) measurable. We could get away with
    imposing only a measurable-space structure on 𝕜 (it doesn't have to be the Borel sigma-algebra of
    a topology); but it seems hard to imagine cases where this extra generality would be useful, and
    allowing it would complicate matters in the most important use cases.

Mathlib/Analysis/Normed/Ring/Seminorm.lean

@@ -329,14 +329,11 @@ variable {R : Type*} [Ring R]
 def equiv (f : MulRingNorm R) (g : MulRingNorm R) :=
   ∃ c : ℝ, 0 < c ∧ (fun x => (f x) ^ c) = g
 
-/- Equivalence of multiplicative ring norms is an equivalence relation
-
-  1. is reflexive-/
+/-- Equivalence of multiplicative ring norms is reflexive. -/
 lemma equiv_refl (f : MulRingNorm R) : equiv f f := by
     exact ⟨1, Real.zero_lt_one, by simp only [Real.rpow_one]⟩
-/- Equivalence of multiplicative ring norms is an equivalence relation
 
- 2. is symmetric-/
+/-- Equivalence of multiplicative ring norms is symmetric. -/
 lemma equiv_symm {f g : MulRingNorm R} (hfg : equiv f g) : equiv g f := by
   rcases hfg with ⟨c, hcpos, h⟩
   use 1/c
@@ -345,9 +342,7 @@ lemma equiv_symm {f g : MulRingNorm R} (hfg : equiv f g) : equiv g f := by
   ext x
   simpa [← congr_fun h x] using Real.rpow_rpow_inv (apply_nonneg f x) (ne_of_lt hcpos).symm
 
-/- Equivalence of multiplicative ring norms is an equivalence relation
-
- 3. is transitive-/
+/-- Equivalence of multiplicative ring norms is transitive. -/
 lemma equiv_trans {f g k : MulRingNorm R} (hfg : equiv f g) (hgk : equiv g k) :
     equiv f k := by
   rcases hfg with ⟨c, hcPos, hfg⟩
@@ -356,7 +351,6 @@ lemma equiv_trans {f g k : MulRingNorm R} (hfg : equiv f g) (hgk : equiv g k) :
   ext x
   rw [Real.rpow_mul (apply_nonneg f x), congr_fun hfg x, congr_fun hgk x]
 
-
 end MulRingNorm
 
 /-- A nonzero ring seminorm on a field `K` is a ring norm. -/
@@ -384,7 +378,7 @@ def normRingNorm (R : Type*) [NonUnitalNormedRing R] : RingNorm R :=
 #align norm_ring_norm normRingNorm
 
 
-/-A multiplicative ring norm satisfies `f n ≤ n` for every `n : ℕ`-/
+/-- A multiplicative ring norm satisfies `f n ≤ n` for every `n : ℕ`. -/
 lemma MulRingNorm_nat_le_nat {R : Type*} [Ring R] (n : ℕ) (f : MulRingNorm R) : f n ≤ n := by
   induction n with
   | zero => simp only [Nat.cast_zero, map_zero, le_refl]

Mathlib/Analysis/NormedSpace/Unitization.lean

@@ -100,8 +100,8 @@ theorem splitMul_injective_of_clm_mul_injective
 variable [RegularNormedAlgebra 𝕜 A]
 variable (𝕜 A)
 
-/- In a `RegularNormedAlgebra`, the map `Unitization.splitMul 𝕜 A` is injective. We will use this
-to pull back the norm from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A`. -/
+/-- In a `RegularNormedAlgebra`, the map `Unitization.splitMul 𝕜 A` is injective.
+We will use this to pull back the norm from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A`. -/
 theorem splitMul_injective : Function.Injective (splitMul 𝕜 A) :=
   splitMul_injective_of_clm_mul_injective (isometry_mul 𝕜 A).injective
 

Mathlib/CategoryTheory/Galois/Decomposition.lean

@@ -54,14 +54,14 @@ non-trivial subobjects which have strictly smaller fiber and conclude by the ind
 
 -/
 
-/- The trivial case if `X` is connected. -/
+/-- The trivial case if `X` is connected. -/
 private lemma has_decomp_connected_components_aux_conn (X : C) [IsConnected X] :
     ∃ (ι : Type) (f : ι → C) (g : (i : ι) → (f i) ⟶ X) (_ : IsColimit (Cofan.mk X g)),
     (∀ i, IsConnected (f i)) ∧ Finite ι := by
   refine ⟨Unit, fun _ ↦ X, fun _ ↦ 𝟙 X, mkCofanColimit _ (fun s ↦ s.inj ()), ?_⟩
   exact ⟨fun _ ↦ inferInstance, inferInstance⟩
 
-/- The trivial case if `X` is initial. -/
+/-- The trivial case if `X` is initial. -/
 private lemma has_decomp_connected_components_aux_initial (X : C) (h : IsInitial X) :
     ∃ (ι : Type) (f : ι → C) (g : (i : ι) → (f i) ⟶ X) (_ : IsColimit (Cofan.mk X g)),
     (∀ i, IsConnected (f i)) ∧ Finite ι := by
@@ -190,11 +190,11 @@ section GaloisRepAux
 
 variable (X : C)
 
-/- The self product of `X` indexed by its fiber. -/
+/-- The self product of `X` indexed by its fiber. -/
 @[simp]
 private noncomputable def selfProd : C := ∏ (fun _ : F.obj X ↦ X)
 
-/- For `g : F.obj X → F.obj X`, this is the element in the fiber of the self product,
+/-- For `g : F.obj X → F.obj X`, this is the element in the fiber of the self product,
 which has at index `x : F.obj X` the element `g x`. -/
 private noncomputable def mkSelfProdFib : F.obj (selfProd F X) :=
   (PreservesProduct.iso F _).inv ((Concrete.productEquiv (fun _ : F.obj X ↦ F.obj X)).symm id)
@@ -209,7 +209,7 @@ private lemma mkSelfProdFib_map_π (t : F.obj X) : F.map (Pi.π _ t) (mkSelfProd
 variable {X} {A : C} [IsConnected A] (u : A ⟶ selfProd F X) [Mono u]
   (a : F.obj A) (h : F.map u a = mkSelfProdFib F X) {F}
 
-/- For each `x : F.obj X`, this is the composition of `u` with the projection at `x`. -/
+/-- For each `x : F.obj X`, this is the composition of `u` with the projection at `x`. -/
 @[simp]
 private noncomputable def selfProdProj (x : F.obj X) : A ⟶ X := u ≫ Pi.π _ x
 
@@ -220,7 +220,7 @@ private lemma selfProdProj_fiber (x : F.obj X) :
   simp only [selfProdProj, selfProd, F.map_comp, FintypeCat.comp_apply, h]
   rw [mkSelfProdFib_map_π F X x]
 
-/- An element `b : F.obj A` defines a permutation of the fiber of `X` by projecting onto the
+/-- An element `b : F.obj A` defines a permutation of the fiber of `X` by projecting onto the
 `F.map u b` factor. -/
 private noncomputable def fiberPerm (b : F.obj A) : F.obj X ≃ F.obj X := by
   let σ (t : F.obj X) : F.obj X := F.map (selfProdProj u t) b
@@ -231,13 +231,13 @@ private noncomputable def fiberPerm (b : F.obj A) : F.obj X ≃ F.obj X := by
   have h' : selfProdProj u t = selfProdProj u s := evaluationInjective_of_isConnected F A X b hs
   rw [← selfProdProj_fiber h s, ← selfProdProj_fiber h t, h']
 
-/- Twisting `u` by `fiberPerm h b` yields an inclusion of `A` into `selfProd F X`. -/
+/-- Twisting `u` by `fiberPerm h b` yields an inclusion of `A` into `selfProd F X`. -/
 private noncomputable def selfProdPermIncl (b : F.obj A) : A ⟶ selfProd F X :=
   u ≫ (Pi.whiskerEquiv (fiberPerm h b) (fun _ => Iso.refl X)).inv
 
 private instance (b : F.obj A) : Mono (selfProdPermIncl h b) := mono_comp _ _
 
-/- Key technical lemma: the twisted inclusion `selfProdPermIncl h b` maps `a` to `F.map u b`. -/
+/-- Key technical lemma: the twisted inclusion `selfProdPermIncl h b` maps `a` to `F.map u b`. -/
 private lemma selfProdTermIncl_fib_eq (b : F.obj A) :
     F.map u b = F.map (selfProdPermIncl h b) a := by
   apply Concrete.Pi.map_ext _ F
@@ -252,9 +252,9 @@ private lemma selfProdTermIncl_fib_eq (b : F.obj A) :
     rw [← map_comp, Pi.map'_comp_π, Category.comp_id, mkSelfProdFib_map_π F X (fiberPerm h b t)]
     rfl
 
-/- There exists an automorphism `f` of `A` that maps `b` to `a`.
-`f` is obtained by considering `u` and `selfProdPermIncl h b`. Both
-are inclusions of `A` into `selfProd F X` mapping `b` respectively `a` to the same element
+/-- There exists an automorphism `f` of `A` that maps `b` to `a`.
+`f` is obtained by considering `u` and `selfProdPermIncl h b`.
+Both are inclusions of `A` into `selfProd F X` mapping `b` respectively `a` to the same element
 in the fiber of `selfProd F X`. Applying `connected_component_unique` yields the result. -/
 private lemma subobj_selfProd_trans (b : F.obj A) : ∃ (f : A ≅ A), F.map f.hom b = a := by
   apply connected_component_unique F b a u (selfProdPermIncl h b)

Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean

@@ -248,7 +248,7 @@ theorem infinite_iff_in_all_ranges {K : Finset V} (C : G.ComponentCompl K) :
 
 end ComponentCompl
 
-/- For a locally finite preconnected graph, the number of components outside of any finite set
+/-- For a locally finite preconnected graph, the number of components outside of any finite set
 is finite. -/
 instance componentCompl_finite [LocallyFinite G] [Gpc : Fact G.Preconnected] (K : Finset V) :
     Finite (G.ComponentCompl K) := by

Mathlib/Data/Fintype/CardEmbedding.lean

@@ -51,7 +51,7 @@ theorem card_embedding_eq {α β : Type*} [Fintype α] [Fintype β] [emb : Finty
       smul_eq_mul, mul_comm]
 #align fintype.card_embedding_eq Fintype.card_embedding_eq
 
-/- The cardinality of embeddings from an infinite type to a finite type is zero.
+/-- The cardinality of embeddings from an infinite type to a finite type is zero.
 This is a re-statement of the pigeonhole principle. -/
 theorem card_embedding_eq_of_infinite {α β : Type*} [Infinite α] [Fintype β] [Fintype (α ↪ β)] :
     ‖α ↪ β‖ = 0 :=

Mathlib/Data/Matrix/ColumnRowPartitioned.lean

@@ -128,13 +128,13 @@ lemma fromRows_ext_iff (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ :
     (B₂ : Matrix m₂ n R) :
     fromRows A₁ A₂ = fromRows B₁ B₂ ↔ A₁ = B₁ ∧ A₂ = B₂ := fromRows_inj.eq_iff
 
-/- A column partioned matrix when transposed gives a row partioned matrix with columns of the
+/-- A column partioned matrix when transposed gives a row partioned matrix with columns of the
 initial matrix tranposed to become rows. -/
 lemma transpose_fromColumns (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
     transpose (fromColumns A₁ A₂) = fromRows (transpose A₁) (transpose A₂) := by
   ext (i | i) j <;> simp
 
-/- A row partioned matrix when transposed gives a column partioned matrix with rows of the initial
+/-- A row partioned matrix when transposed gives a column partioned matrix with rows of the initial
 matrix tranposed to become columns. -/
 lemma transpose_fromRows (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
     transpose (fromRows A₁ A₂) = fromColumns (transpose A₁) (transpose A₂) := by
@@ -252,7 +252,7 @@ lemma fromColumns_mul_fromRows_eq_one_comm (e : n ≃ n₁ ⊕ n₂)
   _ ↔ fromRows B₁ B₂ * fromColumns A₁ A₂ = 1 :=
     (reindex _ _).injective.eq_iff
 
-/- The lemma `fromColumns_mul_fromRows_eq_one_comm` specialized to the case where the index sets n₁
+/-- The lemma `fromColumns_mul_fromRows_eq_one_comm` specialized to the case where the index sets n₁
 and n₂, are the result of subtyping by a predicate and its complement. -/
 lemma equiv_compl_fromColumns_mul_fromRows_eq_one_comm (p : n → Prop)[DecidablePred p]
     (A₁ : Matrix n {i // p i} R) (A₂ : Matrix n {i // ¬p i} R)
@@ -265,15 +265,15 @@ end CommRing
 section Star
 variable [Star R]
 
-/- A column partioned matrix in a Star ring when conjugate transposed gives a row partitioned matrix
-with the columns of the initial matrix conjugate transposed to become rows. -/
+/-- A column partioned matrix in a Star ring when conjugate transposed gives a row partitioned
+matrix with the columns of the initial matrix conjugate transposed to become rows. -/
 lemma conjTranspose_fromColumns_eq_fromRows_conjTranspose (A₁ : Matrix m n₁ R)
     (A₂ : Matrix m n₂ R) :
     conjTranspose (fromColumns A₁ A₂) = fromRows (conjTranspose A₁) (conjTranspose A₂) := by
   ext (_ | _) _ <;> simp
 
-/- A row partioned matrix in a Star ring when conjugate transposed gives a column partitioned matrix
-with the rows of the initial matrix conjugate transposed to become columns. -/
+/-- A row partioned matrix in a Star ring when conjugate transposed gives a column partitioned
+matrix with the rows of the initial matrix conjugate transposed to become columns. -/
 lemma conjTranspose_fromRows_eq_fromColumns_conjTranspose (A₁ : Matrix m₁ n R)
     (A₂ : Matrix m₂ n R) : conjTranspose (fromRows A₁ A₂) =
       fromColumns (conjTranspose A₁) (conjTranspose A₂) := by

Mathlib/LinearAlgebra/FreeModule/Basic.lean

@@ -37,7 +37,7 @@ class Module.Free : Prop where
   exists_basis : Nonempty <| (I : Type v) × Basis I R M
 #align module.free Module.Free
 
-/- If `M` fits in universe `w`, then freeness is equivalent to existence of a basis in that
+/-- If `M` fits in universe `w`, then freeness is equivalent to existence of a basis in that
 universe.
 
 Note that if `M` does not fit in `w`, the reverse direction of this implication is still true as

Mathlib/Mathport/Notation.lean

@@ -340,7 +340,7 @@ partial def matchScoped (lit scopeId : Name) (smatcher : Matcher) : Matcher := g
       else
         return {s with scopeState := binders}
 
-/- Create a `Term` that represents a matcher for `scoped` notation.
+/-- Create a `Term` that represents a matcher for `scoped` notation.
 Fails in the `OptionT` sense if a matcher couldn't be constructed.
 Also returns a delaborator key like in `mkExprMatcher`.
 Reminder: `$lit:ident : (scoped $scopedId:ident => $scopedTerm:Term)` -/

Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

@@ -471,7 +471,7 @@ theorem toWeakDualBCNN_continuous : Continuous (@toWeakDualBCNN Ω _ _ _) :=
   continuous_induced_dom
 #align measure_theory.finite_measure.to_weak_dual_bcnn_continuous MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous
 
-/- Integration of (nonnegative bounded continuous) test functions against finite Borel measures
+/-- Integration of (nonnegative bounded continuous) test functions against finite Borel measures
 depends continuously on the measure. -/
 theorem continuous_testAgainstNN_eval (f : Ω →ᵇ ℝ≥0) :
     Continuous fun μ : FiniteMeasure Ω => μ.testAgainstNN f := by

Mathlib/MeasureTheory/Measure/Haar/Quotient.lean

@@ -255,7 +255,7 @@ theorem MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient [Loc
     apply measure_mono
     exact inter_subset_right _ s
 
-/- Given a normal subgroup `Γ` of a topological group `G` with Haar measure `μ`, which is also
+/-- Given a normal subgroup `Γ` of a topological group `G` with Haar measure `μ`, which is also
   right-invariant, and a finite volume fundamental domain `𝓕`, the quotient map to `G ⧸ Γ`,
   properly normalized, satisfies `QuotientMeasureEqMeasurePreimage`. -/
 @[to_additive "Given a normal
@@ -284,7 +284,7 @@ theorem IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure {𝓕 :
 
 variable (K : PositiveCompacts (G ⧸ Γ))
 
-/- Given a normal subgroup `Γ` of a topological group `G` with Haar measure `μ`, which is also
+/-- Given a normal subgroup `Γ` of a topological group `G` with Haar measure `μ`, which is also
   right-invariant, and a finite volume fundamental domain `𝓕`, the quotient map to `G ⧸ Γ`,
   properly normalized, satisfies `QuotientMeasureEqMeasurePreimage`. -/
 @[to_additive "Given a