doc(NumberTheory): avoid lazy continuation lines (leanprover-community#37571)

We resolve the ambiguity inherent in lazy (un-indented) list item continuation lines by either indenting them or separating them by inserting a newline in the cases where the item continuation was a mistake.

Author: harahu

Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

@@ -356,7 +356,8 @@ Strong recursion principle for a normalised EDS: if we have
 * `P 0`, `P 1`, `P 2`, `P 3`, and `P 4`,
 * for all `m : ℕ` we can prove `P (2 * (m + 3))` from `P k` for all `k < 2 * (m + 3)`, and
 * for all `m : ℕ` we can prove `P (2 * (m + 2) + 1)` from `P k` for all `k < 2 * (m + 2) + 1`,
-  then we have `P n` for all `n : ℕ`.
+
+then we have `P n` for all `n : ℕ`.
 -/
 @[elab_as_elim]
 noncomputable def normEDSRec' {P : ℕ → Sort u}
@@ -372,6 +373,7 @@ noncomputable def normEDSRec' {P : ℕ → Sort u}
   `P (m + 4)`, and `P (m + 5)`, and
 * for all `m : ℕ` we can prove `P (2 * (m + 2) + 1)` from `P (m + 1)`, `P (m + 2)`, `P (m + 3)`,
   and `P (m + 4)`,
+
 then we have `P n` for all `n : ℕ`. -/
 @[elab_as_elim]
 noncomputable def normEDSRec {P : ℕ → Sort u}
@@ -479,6 +481,7 @@ lemma complEDS_odd (m : ℤ) : complEDS b c d k (2 * m + 1) =
 * `P 0`, `P 1`,
 * for all `m : ℕ` we can prove `P (2 * (m + 3))` from `P k` for all `k < 2 * (m + 3)`, and
 * for all `m : ℕ` we can prove `P (2 * (m + 2) + 1)` from `P k` for all `k < 2 * (m + 2) + 1`,
+
 then we have `P n` for all `n : ℕ`. -/
 @[elab_as_elim]
 noncomputable def complEDSRec' {P : ℕ → Sort u} (zero : P 0) (one : P 1)
@@ -493,6 +496,7 @@ noncomputable def complEDSRec' {P : ℕ → Sort u} (zero : P 0) (one : P 1)
   `P (m + 4)`, and `P (m + 5)`, and
 * for all `m : ℕ` we can prove `P (2 * (m + 2) + 1)` from `P (m + 1)`, `P (m + 2)`, `P (m + 3)`,
   and `P (m + 4)`,
+
 then we have `P n` for all `n : ℕ`. -/
 @[elab_as_elim]
 noncomputable def complEDSRec {P : ℕ → Sort u} (zero : P 0) (one : P 1)

Mathlib/NumberTheory/Height/MvPolynomial.lean

@@ -391,6 +391,7 @@ If
 * `q : ι × ι' → MvPolynomial ι K` is a family of homogeneous polynomials of the same degree `M`,
 * `x : ι → K` is such that for all `k : ι`,
   `∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N)`,
+
 then the multiplicative height of `fun j ↦ (p j).eval x` is bounded below by an (explicit) positive
 constant depending only on `q` times the `N`th power of the multiplicative height of `x`.
 A similar statement holds for the logarithmic height.
@@ -428,6 +429,7 @@ open AdmissibleAbsValues
 * `q : ι × ι' → MvPolynomial ι K` is a family of homogeneous polynomials of the same degree `M`,
 * `x : ι → K` is such that for all `k : ι`,
   `∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N)`,
+
 then the multiplicative height of `fun j ↦ (p j).eval x` is bounded below by an (explicit) positive
 constant depending only on `q` times the `N`th power of the multiplicative height of `x`. -/
 theorem mulHeight_eval_ge {M N : ℕ} {q : ι × ι' → MvPolynomial ι K}
@@ -458,6 +460,7 @@ theorem mulHeight_eval_ge {M N : ℕ} {q : ι × ι' → MvPolynomial ι K}
 * `q : ι × ι' → MvPolynomial ι K` is a family of homogeneous polynomials of the same degree `M`,
 * `x : ι → K` is such that for all `k : ι`,
   `∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N)`,
+
 then the multiplicative height of `fun j ↦ (p j).eval x` is bounded below by a positive
 constant depending only on `q` times the `N`th power of the multiplicative height of `x`.
 
@@ -479,6 +482,7 @@ open Real in
 * `q : ι × ι' → MvPolynomial ι K` is a family of homogeneous polynomials of the same degree `M`,
 * `x : ι → K` is such that for all `k : ι`,
   `∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N)`,
+
 then the logarithmic height of `fun j ↦ (p j).eval x` is bounded below by an (explicit)
 constant depending only on `q` plus `N` times the logarithmic height of `x`. -/
 theorem logHeight_eval_ge {M N : ℕ} {q : ι × ι' → MvPolynomial ι K}
@@ -500,6 +504,7 @@ theorem logHeight_eval_ge {M N : ℕ} {q : ι × ι' → MvPolynomial ι K}
 * `q : ι × ι' → MvPolynomial ι K` is a family of homogeneous polynomials of the same degree `M`,
 * `x : ι → K` is such that for all `k : ι`,
   `∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N)`,
+
 then the logarithmic height of `fun j ↦ (p j).eval x` is bounded below by a
 constant plus `N` times the logarithmic height of `x`.
 

Mathlib/NumberTheory/KummerDedekind.lean

@@ -17,6 +17,7 @@ the ring of integers. This states the following: assume we are given
   - A prime ideal `I` of Dedekind domain `R`
   - An `R`-algebra `S` that is a Dedekind Domain
   - An `α : S` that is integral over `R` with minimal polynomial `f`
+
 If the conductor `𝓒` of `x` is such that `𝓒 ∩ R` is coprime to `I` then the prime
 factorisations of `I * S` and `f mod I` have the same shape, i.e. they have the same number of
 prime factors, and each prime factors of `I * S` can be paired with a prime factor of `f mod I` in

Mathlib/NumberTheory/ModularForms/Discriminant.lean

@@ -21,7 +21,7 @@ function, and proves its key properties including invariance under the generator
 ## Main definitions
 
 * `ModularForm.discriminant`: The modular discriminant function `Δ(z) = η(z) ^ 24`, which can also
-be expressed as `q * ∏' (1 - q ^ (n + 1)) ^ 24` where `q = e ^ (2πiz)`.
+  be expressed as `q * ∏' (1 - q ^ (n + 1)) ^ 24` where `q = e ^ (2πiz)`.
 
 ## Main results
 

Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Transform.lean

@@ -43,7 +43,7 @@ the action of `S = [[0, -1], [1, 0]]`.
 The proof of `G2_S_transform` is the heart of this file. The strategy is:
 
 1. **Write as absolutely convergent series**: Express `G2` as an absolutely convergent double sum
-  by adding and subtracting telescoping terms:
+   by adding and subtracting telescoping terms:
    `G₂(z) = 2ζ(2) + ∑' m n, 1/((mz+n)²(mz+n+1)) + δ(m,n)`
    where `δ` is a correction for boundary terms.
 

Mathlib/NumberTheory/NumberField/FractionalIdeal.lean

@@ -17,11 +17,11 @@ Prove some results on the fractional ideals of number fields.
 
 ## Main definitions and results
 
-  * `NumberField.basisOfFractionalIdeal`: A `ℚ`-basis of `K` that spans `I` over `ℤ` where `I` is
-    a fractional ideal of a number field `K`.
-  * `NumberField.det_basisOfFractionalIdeal_eq_absNorm`: for `I` a fractional ideal of a number
-    field `K`, the absolute value of the determinant of the base change from `integralBasis` to
-    `basisOfFractionalIdeal I` is equal to the norm of `I`.
+* `NumberField.basisOfFractionalIdeal`: A `ℚ`-basis of `K` that spans `I` over `ℤ` where `I` is
+  a fractional ideal of a number field `K`.
+* `NumberField.det_basisOfFractionalIdeal_eq_absNorm`: for `I` a fractional ideal of a number
+  field `K`, the absolute value of the determinant of the base change from `integralBasis` to
+  `basisOfFractionalIdeal I` is equal to the norm of `I`.
 -/
 
 @[expose] public section

Mathlib/NumberTheory/RamificationInertia/Basic.lean

@@ -33,6 +33,7 @@ Often the above theory is set up in the case where:
 * `S` is the integral closure of `R` in `L`,
 * `p` and `P` are maximal ideals,
 * `P` is an ideal lying over `p`
+
 We will try to relax the above hypotheses as much as possible.
 
 ## Notation

Mathlib/NumberTheory/RamificationInertia/Inertia.lean

@@ -24,6 +24,7 @@ Often the above theory is set up in the case where:
 * `S` is the integral closure of `R` in `L`,
 * `p` and `P` are maximal ideals,
 * `P` is an ideal lying over `p`
+
 We will try to relax the above hypotheses as much as possible.
 
 ## Notation

Mathlib/NumberTheory/RamificationInertia/Ramification.lean

@@ -24,6 +24,7 @@ Often the above theory is set up in the case where:
 * `S` is the integral closure of `R` in `L`,
 * `p` and `P` are maximal ideals,
 * `P` is an ideal lying over `p`.
+
 We will try to relax the above hypotheses as much as possible.
 
 ## Notation