fix(GroupTheory): avoid unintentional list item continuation lines (leanprover-community#37615)

Currently, all of the sentence fragments that we're separating with a newline are rendering as part of the preceding list item. The addition of these newlines renders the sentence fragments as a separate paragraph following the list.

Author: harahu

Mathlib/GroupTheory/Descent.lean

@@ -29,6 +29,7 @@ and constants `a, b, c : ℝ` such that
 * for all `x : G`, `h (f x) ≥ b * h x - c`,
 * for all `B : ℝ`, there are only finitely many `x : G` such that `h x ≤ B`, and
 * `0 ≤ a < b`,
+
 then `G` is finitely generated. See `Group.fg_of_descent` / `AddGroup.fg_of_descent`.
 
 We use this to deduce a more specific version when `G` is commutative and `f` is the `n`th power
@@ -94,13 +95,15 @@ If `G` is a commutative group and `n : ℕ`, `h : G → ℝ` satisfy
 * for all `g x : G`, `h x ≤ a * h (g * x) + c g`,
 * for all `x : G`, `h (x ^ n) ≥ b * h x - c₀`,
 * for all `B : ℝ`, there are only finitely many `x : G` such that `h x ≤ B`,
+
 where `0 ≤ a < b` and `c₀` are real numbers, `c : G → ℝ`, then `G` is finitely generated.
 -/
 @[to_additive /-- If `G` is a commutative additive group and `n : ℕ`, `h : G → ℝ` satisfy
 * `G / n • G` is finite,
 * for all `g x : G`, `h x ≤ a * h (g + x) + c g`,
 * for all `x : G`, `h (n • x) ≥ b * h x - c₀`,
 * for all `B : ℝ`, there are only finitely many `x : G` such that `h x ≤ B`,
+
 where `0 ≤ a < b` and `c₀` are real numbers, `c : G → ℝ`, then `G` is finitely generated. -/]
 theorem CommGroup.fg_of_descent {G : Type*} [CommGroup G] {n : ℕ} {h : G → ℝ} {a b c₀ : ℝ}
     {c : G → ℝ} (ha : 0 ≤ a) (H₀ : a < b) (H₁ : (powMonoidHom (α := G) n).range.FiniteIndex)
@@ -129,13 +132,15 @@ If `G` is a commutative group and `n : ℕ`, `h : G → ℝ` satisfy
 * `0 ≤ h x` for all `x : G`,
 * there is `C : ℝ` such that for all `x y : G`, `|h (x * y) + h(x / y) - 2 * (h x + h y)| ≤ C`,
 * for all `B : ℝ`, there are only finitely many `x : G` such that `h x ≤ B`,
+
 then `G` is finitely generated.
 -/
 @[to_additive /-- If `G` is a commutative additive group and `n : ℕ`, `h : G → ℝ` satisfy
 * `G / 2 • G` is finite,
 * `0 ≤ h x` for all `x : G`,
 * there is `C : ℝ` such that for all `x y : G`, `|h (x + y) + h(x - y) - 2 * (h x + h y)| ≤ C`,
 * for all `B : ℝ`, there are only finitely many `x : G` such that `h x ≤ B`,
+
 then `G` is finitely generated. -/]
 theorem CommGroup.fg_of_descent' {G : Type*} [CommGroup G] {h : G → ℝ} {C : ℝ}
     (H₁ : (powMonoidHom (α := G) 2).range.FiniteIndex) (H₂ : ∀ x, 0 ≤ h x)