docs(*): fix incorrect --/ in docstrings (#17701)

Fix incorrect syntax in docstrings.

counterexamples/char_p_zero_ne_char_zero.lean

@@ -16,7 +16,7 @@ The reverse implication holds for any `add_left_cancel_monoid R` with `1`, by `c
 This file shows that there are semiring `R` for which `char_p R 0` holds and `char_zero R` does not.
 
 The example is `{0, 1}` with saturating addition.
---/
+-/
 
 local attribute [semireducible] with_zero
 

src/algebra/direct_sum/module.lean

@@ -312,7 +312,7 @@ by simp
 
 /-- When indexed by only two distinct elements, `direct_sum.is_internal` implies
 the two submodules are complementary. Over a `ring R`, this is true as an iff, as
-`direct_sum.is_internal_iff_is_compl`. --/
+`direct_sum.is_internal_iff_is_compl`. -/
 lemma is_internal.is_compl {A : ι → submodule R M} {i j : ι} (hij : i ≠ j)
   (h : (set.univ : set ι) = {i, j}) (hi : is_internal A) : is_compl (A i) (A j) :=
 ⟨hi.submodule_independent.pairwise_disjoint hij,

src/algebra/star/basic.lean

@@ -188,7 +188,7 @@ def star_semigroup_of_comm {R : Type*} [comm_monoid R] : star_semigroup R :=
 section
 local attribute [instance] star_semigroup_of_comm
 
-/-- Note that since `star_semigroup_of_comm` is reducible, `simp` can already prove this. --/
+/-- Note that since `star_semigroup_of_comm` is reducible, `simp` can already prove this. -/
 lemma star_id_of_comm {R : Type*} [comm_semiring R] {x : R} : star x = x := rfl
 
 end

src/analysis/inner_product_space/basic.lean

@@ -1235,7 +1235,7 @@ lemma orthonormal.comp_linear_isometry_equiv {v : ι → E} (hv : orthonormal 
 hv.comp_linear_isometry f.to_linear_isometry
 
 /-- A linear isometric equivalence, applied with `basis.map`, preserves the property of being
-orthonormal. --/
+orthonormal. -/
 lemma orthonormal.map_linear_isometry_equiv {v : basis ι 𝕜 E} (hv : orthonormal 𝕜 v)
   (f : E ≃ₗᵢ[𝕜] E') : orthonormal 𝕜 (v.map f.to_linear_equiv) :=
 hv.comp_linear_isometry_equiv f

src/analysis/inner_product_space/pi_L2.lean

@@ -287,7 +287,7 @@ begin
     euclidean_space.inner_single_left, euclidean_space.single_apply, map_one, one_mul],
 end
 
-/-- The `basis ι 𝕜 E` underlying the `orthonormal_basis` --/
+/-- The `basis ι 𝕜 E` underlying the `orthonormal_basis` -/
 protected def to_basis (b : orthonormal_basis ι 𝕜 E) : basis ι 𝕜 E :=
 basis.of_equiv_fun b.repr.to_linear_equiv
 

src/category_theory/eq_to_hom.lean

@@ -130,7 +130,7 @@ begin
   simpa using h_map X Y f
 end
 
-/-- Two morphisms are conjugate via eq_to_hom if and only if they are heterogeneously equal. --/
+/-- Two morphisms are conjugate via eq_to_hom if and only if they are heterogeneously equal. -/
 lemma conj_eq_to_hom_iff_heq {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) :
   f = eq_to_hom h ≫ g ≫ eq_to_hom h'.symm ↔ f == g :=
 by { cases h, cases h', simp }

src/combinatorics/simple_graph/basic.lean

@@ -427,7 +427,7 @@ the second dart's first vertex. -/
 def dart_adj (d d' : G.dart) : Prop := d.snd = d'.fst
 
 /-- For a given vertex `v`, this is the bijective map from the neighbor set at `v`
-to the darts `d` with `d.fst = v`. --/
+to the darts `d` with `d.fst = v`. -/
 @[simps] def dart_of_neighbor_set (v : V) (w : G.neighbor_set v) : G.dart :=
 ⟨(v, w), w.property⟩
 
@@ -1274,7 +1274,7 @@ abbreviation to_embedding : G ↪g G' := f.to_rel_embedding
 /-- An isomorphism of graphs gives rise to a homomorphism of graphs. -/
 abbreviation to_hom : G →g G' := f.to_embedding.to_hom
 
-/-- The inverse of a graph isomorphism. --/
+/-- The inverse of a graph isomorphism. -/
 abbreviation symm : G' ≃g G := f.symm
 
 lemma map_adj_iff {v w : V} : G'.adj (f v) (f w) ↔ G.adj v w := f.map_rel_iff

src/combinatorics/simple_graph/subgraph.lean

@@ -116,7 +116,7 @@ G'.adj_sub h
 protected lemma adj.coe {H : G.subgraph} {u v : V} (h : H.adj u v) :
   H.coe.adj ⟨u, H.edge_vert h⟩ ⟨v, H.edge_vert h.symm⟩ := h
 
-/-- A subgraph is called a *spanning subgraph* if it contains all the vertices of `G`. --/
+/-- A subgraph is called a *spanning subgraph* if it contains all the vertices of `G`. -/
 def is_spanning (G' : subgraph G) : Prop := ∀ (v : V), v ∈ G'.verts
 
 lemma is_spanning_iff {G' : subgraph G} : G'.is_spanning ↔ G'.verts = set.univ :=

src/combinatorics/young/semistandard_tableau.lean

@@ -46,7 +46,7 @@ numbers, such that the entries in each row are weakly increasing (left to right)
 in each column are strictly increasing (top to bottom).
 
 Here, an SSYT is represented as an unrestricted function `ℕ → ℕ → ℕ` that, for reasons
-of extensionality, is required to vanish outside `μ`. --/
+of extensionality, is required to vanish outside `μ`. -/
 structure ssyt (μ : young_diagram) :=
 (entry : ℕ → ℕ → ℕ)
 (row_weak' : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry i j1 ≤ entry i j2)
@@ -105,7 +105,7 @@ lemma col_weak {μ : young_diagram} (T : ssyt μ) {i1 i2 j : ℕ}
   (hi : i1 ≤ i2) (cell : (i2, j) ∈ μ) : T i1 j ≤ T i2 j :=
 by { cases eq_or_lt_of_le hi, subst h, exact le_of_lt (T.col_strict h cell) }
 
-/-- The "highest weight" SSYT of a given shape is has all i's in row i, for each i. --/
+/-- The "highest weight" SSYT of a given shape is has all i's in row i, for each i. -/
 def highest_weight (μ : young_diagram) : ssyt μ :=
 { entry := λ i j, if (i, j) ∈ μ then i else 0,
   row_weak' := λ i j1 j2 hj hcell,

src/data/rel.lean

@@ -31,7 +31,7 @@ Relations are also known as set-valued functions, or partial multifunctions.
 
 variables {α β γ : Type*}
 
-/-- A relation on `α` and `β`, aka a set-valued function, aka a partial multifunction --/
+/-- A relation on `α` and `β`, aka a set-valued function, aka a partial multifunction -/
 @[derive complete_lattice, derive inhabited]
 def rel (α β : Type*) := α → β → Prop
 

src/field_theory/ratfunc.lean

@@ -567,7 +567,7 @@ lemma coe_map_ring_hom_eq_coe_map [ring_hom_class F R[X] S[X]] (φ : F)
 -- TODO: Generalize to `fun_like` classes,
 /-- Lift an monoid with zero homomorphism `R[X] →*₀ G₀` to a `ratfunc R →*₀ G₀`
 on the condition that `φ` maps non zero divisors to non zero divisors,
-by mapping both the numerator and denominator and quotienting them. --/
+by mapping both the numerator and denominator and quotienting them. -/
 def lift_monoid_with_zero_hom (φ : R[X] →*₀ G₀) (hφ : R[X]⁰ ≤ G₀⁰.comap φ) :
   ratfunc R →*₀ G₀ :=
 { to_fun := λ f, ratfunc.lift_on f (λ p q, φ p / (φ q)) $ λ p q p' q' hq hq' h, begin
@@ -609,7 +609,7 @@ begin
 end
 
 /-- Lift an injective ring homomorphism `R[X] →+* L` to a `ratfunc R →+* L`
-by mapping both the numerator and denominator and quotienting them. --/
+by mapping both the numerator and denominator and quotienting them. -/
 def lift_ring_hom (φ : R[X] →+* L) (hφ : R[X]⁰ ≤ L⁰.comap φ) : ratfunc R →+* L :=
 { map_add' := λ x y, by { simp only [monoid_with_zero_hom.to_fun_eq_coe],
     casesI subsingleton_or_nontrivial R,
@@ -783,7 +783,7 @@ lemma coe_map_alg_hom_eq_coe_map (φ : K[X] →ₐ[S] R[X])
   (map_alg_hom φ hφ : ratfunc K → ratfunc R) = map φ hφ := rfl
 
 /-- Lift an injective algebra homomorphism `K[X] →ₐ[S] L` to a `ratfunc K →ₐ[S] L`
-by mapping both the numerator and denominator and quotienting them. --/
+by mapping both the numerator and denominator and quotienting them. -/
 def lift_alg_hom : ratfunc K →ₐ[S] L :=
 { commutes' := λ r, by simp_rw [ring_hom.to_fun_eq_coe, alg_hom.to_ring_hom_eq_coe,
     algebra_map_apply r, lift_ring_hom_apply_div, alg_hom.coe_to_ring_hom, map_one,

src/group_theory/free_group.lean

@@ -425,7 +425,7 @@ instance : has_mul (free_group α) :=
     (λ L₁ L₂ H, quot.induction_on y $ λ L₃, quot.sound $ red.step.append_right H)⟩
 @[simp, to_additive] lemma mul_mk : mk L₁ * mk L₂ = mk (L₁ ++ L₂) := rfl
 
-/-- Transform a word representing a free group element into a word representing its inverse. --/
+/-- Transform a word representing a free group element into a word representing its inverse. -/
 @[to_additive "Transform a word representing a free group element into a word representing its
 negative."]
 def inv_rev (w : list (α × bool)) : list (α × bool) :=
@@ -1073,7 +1073,7 @@ section metric
 
 variable [decidable_eq α]
 
-/-- The length of reduced words provides a norm on a free group. --/
+/-- The length of reduced words provides a norm on a free group. -/
 @[to_additive "The length of reduced words provides a norm on an additive free group."]
 def norm (x : free_group α) : ℕ := x.to_word.length
 

src/logic/embedding/basic.lean

@@ -135,7 +135,7 @@ protected noncomputable def equiv_of_surjective {α β} (f : α ↪ β) (hf : su
   α ≃ β :=
 equiv.of_bijective f ⟨f.injective, hf⟩
 
-/-- There is always an embedding from an empty type. --/
+/-- There is always an embedding from an empty type. -/
 protected def of_is_empty {α β} [is_empty α] : α ↪ β :=
 ⟨is_empty_elim, is_empty_elim⟩
 

src/measure_theory/integral/interval_integral.lean

@@ -2514,7 +2514,7 @@ Change of variables, general form. If `f` is continuous on `[a, b]` and has
 right-derivative `f'` in `(a, b)`, `g` is continuous on `f '' (a, b)` and integrable on
 `f '' [a, b]`, and `f' x • (g ∘ f) x` is integrable on `[a, b]`,
 then we can substitute `u = f x` to get `∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`.
---/
+-/
 theorem integral_comp_smul_deriv''' {f f' : ℝ → ℝ} {g : ℝ → E}
   (hf : continuous_on f [a, b])
   (hff' : ∀ x ∈ Ioo (min a b) (max a b), has_deriv_within_at f (f' x) (Ioi x) x)

src/number_theory/wilson.lean

@@ -29,7 +29,7 @@ open_locale nat
 namespace nat
 variable {n : ℕ}
 
-/-- For `n ≠ 1`, `(n-1)!` is congruent to `-1` modulo `n` only if n is prime. --/
+/-- For `n ≠ 1`, `(n-1)!` is congruent to `-1` modulo `n` only if n is prime. -/
 lemma prime_of_fac_equiv_neg_one
   (h : ((n - 1)! : zmod n) = -1) (h1 : n ≠ 1) : prime n :=
 begin
@@ -43,7 +43,7 @@ begin
   rw [←zmod.nat_coe_zmod_eq_zero_iff_dvd, cast_add, cast_one, h, add_left_neg],
 end
 
-/-- **Wilson's Theorem**: For `n ≠ 1`, `(n-1)!` is congruent to `-1` modulo `n` iff n is prime. --/
+/-- **Wilson's Theorem**: For `n ≠ 1`, `(n-1)!` is congruent to `-1` modulo `n` iff n is prime. -/
 theorem prime_iff_fac_equiv_neg_one (h : n ≠ 1) :
   prime n ↔ ((n - 1)! : zmod n) = -1 :=
 begin

src/order/filter/basic.lean

@@ -658,7 +658,7 @@ begin
   exact ⟨λ i, s i, λ i, (s i).2, pairwise.set_of_subtype _ _ hd⟩
 end
 
-/-- There is exactly one filter on an empty type. --/
+/-- There is exactly one filter on an empty type. -/
 instance unique [is_empty α] : unique (filter α) :=
 { default := ⊥, uniq := filter_eq_bot_of_is_empty }
 

src/order/hom/basic.lean

@@ -453,7 +453,7 @@ rel_embedding.of_map_rel_iff f hf
 @[simp] lemma coe_of_map_le_iff {α β} [partial_order α] [preorder β] {f : α → β} (h) :
   ⇑(of_map_le_iff f h) = f := rfl
 
-/-- A strictly monotone map from a linear order is an order embedding. --/
+/-- A strictly monotone map from a linear order is an order embedding. -/
 def of_strict_mono {α β} [linear_order α] [preorder β] (f : α → β)
   (h : strict_mono f) : α ↪o β :=
 of_map_le_iff f (λ _ _, h.le_iff_le)
@@ -654,7 +654,7 @@ by { ext, simp }
 by { ext, simp }
 
 /-- To show that `f : α → β`, `g : β → α` make up an order isomorphism of linear orders,
-    it suffices to prove `cmp a (g b) = cmp (f a) b`. --/
+    it suffices to prove `cmp a (g b) = cmp (f a) b`. -/
 def of_cmp_eq_cmp {α β} [linear_order α] [linear_order β] (f : α → β) (g : β → α)
   (h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b) : α ≃o β :=
 have gf : ∀ (a : α), a = g (f a) := by { intro, rw [←cmp_eq_eq_iff, h, cmp_self_eq_eq] },

src/ring_theory/fractional_ideal.lean

@@ -148,7 +148,7 @@ end set_like
 @[simp, norm_cast] lemma coe_mk (I : submodule R P) (hI : is_fractional S I) :
   (subtype.mk I hI : submodule R P) = I := rfl
 
-/-! Transfer instances from `submodule R P` to `fractional_ideal S P`. --/
+/-! Transfer instances from `submodule R P` to `fractional_ideal S P`. -/
 instance (I : fractional_ideal S P) : add_comm_group I := submodule.add_comm_group ↑I
 instance (I : fractional_ideal S P) : module R I := submodule.module ↑I
 

src/tactic/congrm.lean

@@ -136,7 +136,7 @@ end
 (assuming that `lhs` and `rhs` are unifiable with `pat`)
 by applying congruence lemmas until `pat` is a metavariable.
 The subgoals for the leafs are prepended to the goals.
---/
+-/
 meta def equate_with_pattern (pat : expr) : tactic unit := do
 congr_subgoals ← solve1 (equate_with_pattern_core pat),
 gs ← get_goals,

src/topology/category/Top/limits.lean

@@ -1015,7 +1015,7 @@ end
 
 /--
 Cofiltered limits of nonempty compact Hausdorff spaces are nonempty topological spaces.
---/
+-/
 lemma nonempty_limit_cone_of_compact_t2_cofiltered_system
   [is_cofiltered J]
   [Π (j : J), nonempty (F.obj j)]