doc: write n-th instead of n'th (leanprover-community#29433)

This seems to be the more correct spelling.

Author: harahu

Archive/Wiedijk100Theorems/Partition.lean

@@ -32,7 +32,7 @@ equal:
 
 $$\prod_{i=0}^\infty \frac {1}{1-X^{2i+1}} = \prod_{i=0}^\infty (1+X^{i+1})$$
 
-In fact, we do not take a limit: it turns out that comparing the `n`'th coefficients of the partial
+In fact, we do not take a limit: it turns out that comparing the `n`-th coefficients of the partial
 products up to `m := n + 1` is sufficient.
 
 In particular, we

Mathlib/Algebra/Polynomial/Sequence.lean

@@ -38,9 +38,9 @@ namespace Polynomial
 
 /-- A sequence of polynomials such that the polynomial at index `i` has degree `i`. -/
 structure Sequence [Semiring R] where
-  /-- The `i`'th element in the sequence. Use `S i` instead, defined via `CoeFun`. -/
+  /-- The `i`-th element in the sequence. Use `S i` instead, defined via `CoeFun`. -/
   protected elems' : ℕ → R[X]
-  /-- The `i`'th element in the sequence has degree `i`. Use `S.degree_eq` instead. -/
+  /-- The `i`-th element in the sequence has degree `i`. Use `S.degree_eq` instead. -/
   protected degree_eq' (i : ℕ) : (elems' i).degree = i
 
 attribute [coe] Sequence.elems'
@@ -174,7 +174,7 @@ variable (hCoeff : ∀ i, IsUnit (S i).leadingCoeff)
 noncomputable def basis : Basis ℕ R R[X] :=
   Basis.mk S.linearIndependent <| eq_top_iff.mp <| S.span hCoeff
 
-/-- The `i`'th basis vector is the `i`'th polynomial in the sequence. -/
+/-- The `i`-th basis vector is the `i`-th polynomial in the sequence. -/
 @[simp]
 lemma basis_eq_self (i : ℕ) : S.basis hCoeff i = S i := Basis.mk_apply _ _ _
 

Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean

@@ -26,7 +26,7 @@ as a linear map. This is used in particular in the proof of the Lindemann-Weiers
 * `Polynomial.sumIDeriv_map`: `Polynomial.sumIDeriv` commutes with `Polynomial.map`
 * `Polynomial.sumIDeriv_derivative`: `Polynomial.sumIDeriv` commutes with `Polynomial.derivative`
 * `Polynomial.sumIDeriv_eq_self_add`: `sumIDeriv p = p + derivative (sumIDeriv p)`
-* `Polynomial.exists_iterate_derivative_eq_factorial_smul`: the `k`'th iterated derivative of a
+* `Polynomial.exists_iterate_derivative_eq_factorial_smul`: the `k`-th iterated derivative of a
   polynomial has a common factor `k!`
 * `Polynomial.aeval_iterate_derivative_of_lt`, `Polynomial.aeval_iterate_derivative_self`,
   `Polynomial.aeval_iterate_derivative_of_ge`: applying `Polynomial.aeval` to iterated derivatives

Mathlib/Computability/AkraBazzi/AkraBazzi.lean

@@ -18,7 +18,7 @@ coefficients, and the `b_i`'s are reals `∈ (0,1)`. (Note that this can be impr
 `O(n / (log n)^(1+ε))`, this is left as future work.) These recurrences arise mainly in the
 analysis of divide-and-conquer algorithms such as mergesort or Strassen's algorithm for matrix
 multiplication.  This class of algorithms works by dividing an instance of the problem of size `n`,
-into `k` smaller instances, where the `i`'th instance is of size roughly `b_i n`, and calling itself
+into `k` smaller instances, where the `i`-th instance is of size roughly `b_i n`, and calling itself
 recursively on those smaller instances. `T(n)` then represents the running time of the algorithm,
 and `g(n)` represents the running time required to actually divide up the instance and process the
 answers that come out of the recursive calls. Since virtually all such algorithms produce instances

Mathlib/GroupTheory/Nilpotent.lean

@@ -368,7 +368,7 @@ variable [hG : IsNilpotent G]
 variable (G) in
 open scoped Classical in
 /-- The nilpotency class of a nilpotent group is the smallest natural `n` such that
-the `n`'th term of the upper central series is `G`. -/
+the `n`-th term of the upper central series is `G`. -/
 noncomputable def Group.nilpotencyClass : ℕ := Nat.find (IsNilpotent.nilpotent G)
 
 open scoped Classical in
@@ -388,7 +388,7 @@ theorem upperCentralSeries_eq_top_iff_nilpotencyClass_le {n : ℕ} :
 
 open scoped Classical in
 /-- The nilpotency class of a nilpotent `G` is equal to the smallest `n` for which an ascending
-central series reaches `G` in its `n`'th term. -/
+central series reaches `G` in its `n`-th term. -/
 theorem least_ascending_central_series_length_eq_nilpotencyClass :
     Nat.find ((nilpotent_iff_finite_ascending_central_series G).mp hG) =
     Group.nilpotencyClass G := by
@@ -401,7 +401,7 @@ theorem least_ascending_central_series_length_eq_nilpotencyClass :
 
 open scoped Classical in
 /-- The nilpotency class of a nilpotent `G` is equal to the smallest `n` for which the descending
-central series reaches `⊥` in its `n`'th term. -/
+central series reaches `⊥` in its `n`-th term. -/
 theorem least_descending_central_series_length_eq_nilpotencyClass :
     Nat.find ((nilpotent_iff_finite_descending_central_series G).mp hG) =
     Group.nilpotencyClass G := by

Mathlib/LinearAlgebra/Basis/Defs.lean

@@ -656,7 +656,7 @@ section Coord
 
 variable (i : ι)
 
-/-- `b.coord i` is the linear function giving the `i`'th coordinate of a vector
+/-- `b.coord i` is the linear function giving the `i`-th coordinate of a vector
 with respect to the basis `b`.
 
 `b.coord i` is an element of the dual space. In particular, for

Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean

@@ -36,14 +36,14 @@ of `1` in `L`.
   are `n` `n`th roots of unity in `L`.
 
 * `cyclotomicCharacter L p : (L ≃+* L) →* ℤ_[p]ˣ` sends `g` to the unique `j` such
-  that `g(ζ) = ζ ^ (j mod pⁱ)` for all `pⁱ`'th roots of unity `ζ`.
+  that `g(ζ) = ζ ^ (j mod pⁱ)` for all `pⁱ`-th roots of unity `ζ`.
 
   Note: This is defined to be the trivial character if `L` has no enough roots of unity.
 
 ## Implementation note
 
 In theory this could be set up as some theory about monoids, being a character
-on monoid isomorphisms, but under the hypotheses that the `n`'th roots of unity
+on monoid isomorphisms, but under the hypotheses that the `n`-th roots of unity
 are cyclic. The advantage of sticking to integral domains is that finite subgroups
 are guaranteed to be cyclic, so the weaker assumption that there are `n` `n`th
 roots of unity is enough. All the applications I'm aware of are when `L` is a
@@ -84,8 +84,8 @@ theorem rootsOfUnity.integer_power_of_ringEquiv' (g : L ≃+* L) :
   simpa using rootsOfUnity.integer_power_of_ringEquiv n g
 
 /-- `modularCyclotomicCharacter_aux g n` is a non-canonical auxiliary integer `j`,
-  only well-defined modulo the number of `n`'th roots of unity in `L`, such that `g(ζ)=ζ^j`
-  for all `n`'th roots of unity `ζ` in `L`. -/
+  only well-defined modulo the number of `n`-th roots of unity in `L`, such that `g(ζ)=ζ^j`
+  for all `n`-th roots of unity `ζ` in `L`. -/
 noncomputable def modularCyclotomicCharacter.aux (g : L ≃+* L) (n : ℕ) [NeZero n] : ℤ :=
   (rootsOfUnity.integer_power_of_ringEquiv n g).choose
 
@@ -115,7 +115,7 @@ theorem modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow
 
 /-- If `g` is a ring automorphism of `L`, and `n : ℕ+`, then
   `modularCyclotomicCharacter.toFun n g` is the `j : ZMod d` such that `g(ζ)=ζ^j` for all
-  `n`'th roots of unity. Here `d` is the number of `n`th roots of unity in `L`. -/
+  `n`-th roots of unity. Here `d` is the number of `n`th roots of unity in `L`. -/
 noncomputable def modularCyclotomicCharacter.toFun (n : ℕ) [NeZero n] (g : L ≃+* L) :
     ZMod (Fintype.card (rootsOfUnity n L)) :=
   modularCyclotomicCharacter.aux g n
@@ -179,7 +179,7 @@ variable (L)
 
 /-- Given a positive integer `n`, `modularCyclotomicCharacter' n` is a
 multiplicative homomorphism from the automorphisms of a field `L` to `(ℤ/dℤ)ˣ`,
-where `d` is the number of `n`'th roots of unity in `L`. It is uniquely
+where `d` is the number of `n`-th roots of unity in `L`. It is uniquely
 characterised by the property that `g(ζ)=ζ^(modularCyclotomicCharacter n g)`
 for `g` an automorphism of `L` and `ζ` an `n`th root of unity. -/
 noncomputable
@@ -296,7 +296,7 @@ variable (L) in
 /--
 Suppose `L` is a domain containing all `pⁱ`-th primitive roots with `p` a (rational) prime.
 If `g` is a ring automorphism of `L`, then `cyclotomicCharacter L p g` is the unique `j : ℤₚ` such
-that `g(ζ) = ζ ^ (j mod pⁱ)` for all `pⁱ`'th roots of unity `ζ`.
+that `g(ζ) = ζ ^ (j mod pⁱ)` for all `pⁱ`-th roots of unity `ζ`.
 
 Note: This is the trivial character when `L` does not contain all `pⁱ`-th primitive roots.
 -/

Mathlib/Tactic/Polyrith.lean

@@ -154,7 +154,7 @@ partial def parse {u : Level} {α : Q(Type u)} (sα : Q(CommSemiring $α))
 
 /-- The possible hypothesis sources for a polyrith proof. -/
 inductive Source where
-  /-- `input n` refers to the `n`'th input `ai` in `polyrith [a1, ..., an]`. -/
+  /-- `input n` refers to the `n`-th input `ai` in `polyrith [a1, ..., an]`. -/
   | input : Nat → Source
   /-- `fvar h` refers to hypothesis `h` from the local context. -/
   | fvar : FVarId → Source