doc(*): add bold in doc strings for named theorems i.e. **mean value …

…theorem** (#8182)

archive/100-theorems-list/16_abel_ruffini.lean

@@ -161,6 +161,7 @@ theorem not_solvable_by_rad' (x : ℂ) (hx : aeval x (Φ ℚ 4 2) = 0) :
   ¬ is_solvable_by_rad ℚ x :=
 by apply not_solvable_by_rad 4 2 2 x hx; norm_num
 
+/-- **Abel-Ruffini Theorem** -/
 theorem exists_not_solvable_by_rad : ∃ x : ℂ, is_algebraic ℚ x ∧ ¬ is_solvable_by_rad ℚ x :=
 begin
   obtain ⟨x, hx⟩ := exists_root_of_splits (algebra_map ℚ ℂ)

archive/100-theorems-list/42_inverse_triangle_sum.lean

@@ -21,6 +21,7 @@ discrete_sum
 open_locale big_operators
 open finset
 
+/-- **Sum of the Reciprocals of the Triangular Numbers** -/
 lemma inverse_triangle_sum :
   ∀ n, ∑ k in range n, (2 : ℚ) / (k * (k + 1)) = if n = 0 then 0 else 2 - (2 : ℚ) / n :=
 begin

archive/100-theorems-list/57_herons_formula.lean

@@ -29,7 +29,7 @@ variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P]
 
 include V
 
-/-- Heron's formula: The area of a triangle with side lengths `a`, `b`, and `c` is
+/-- **Heron's formula**: The area of a triangle with side lengths `a`, `b`, and `c` is
   `√(s * (s - a) * (s - b) * (s - c))` where `s = (a + b + c) / 2` is the semiperimeter.
   We show this by equating this formula to `a * b * sin γ`, where `γ` is the angle opposite
   the side `c`.

archive/100-theorems-list/70_perfect_numbers.lean

@@ -76,7 +76,7 @@ begin
   rw [pow_succ', mul_assoc, ← hm],
 end
 
-/-- Euler's theorem that even perfect numbers can be factored as a
+/-- **Perfect Number Theorem**: Euler's theorem that even perfect numbers can be factored as a
   power of two times a Mersenne prime. -/
 theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : even n) (perf : perfect n) :
   ∃ (k : ℕ), prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1) :=

archive/100-theorems-list/73_ascending_descending_sequences.lean

@@ -28,8 +28,8 @@ open function finset
 open_locale classical
 
 /--
-Given a sequence of more than `r * s` distinct values, there is an increasing sequence of length
-longer than `r` or a decreasing sequence of length longer than `s`.
+**Erdős–Szekeres Theorem**: Given a sequence of more than `r * s` distinct values, there is an
+increasing sequence of length longer than `r` or a decreasing sequence of length longer than `s`.
 
 Proof idea:
 We label each value in the sequence with two numbers specifying the longest increasing

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -513,7 +513,7 @@ begin
   dsimp only [decreasing_sequence], rw hnm
 end
 
-/-- A cube cannot be cubed. -/
+/-- **Dissection of Cubes**: A cube cannot be cubed. -/
 theorem cannot_cube_a_cube :
   ∀{n : ℕ}, n ≥ 3 →                              -- In ℝ^n for n ≥ 3
   ∀{ι : Type} [fintype ι] {cs : ι → cube n},     -- given a finite collection of (hyper)cubes

archive/100-theorems-list/83_friendship_graphs.lean

@@ -322,8 +322,8 @@ end
 
 end friendship
 
-/-- We wish to show that a friendship graph has a politician (a vertex adjacent to all others).
-  We proceed by contradiction, and assume the graph has no politician.
+/-- **Friendship theorem**: We wish to show that a friendship graph has a politician (a vertex
+  adjacent to all others). We proceed by contradiction, and assume the graph has no politician.
   We have already proven that a friendship graph with no politician is `d`-regular for some `d`,
   and now we do casework on `d`.
   If the degree is at most 2, we observe by casework that it has a politician anyway.

archive/100-theorems-list/93_birthday_problem.lean

@@ -17,6 +17,7 @@ uses is `fintype.card_embedding_eq`.
 
 local notation `‖` x `‖` := fintype.card x
 
+/-- **Birthday Problem** -/
 theorem birthday :
   2 * ‖fin 23 ↪ fin 365‖ < ‖fin 23 → fin 365‖ ∧ 2 * ‖fin 22 ↪ fin 365‖ > ‖fin 22 → fin 365‖ :=
 begin

archive/100-theorems-list/9_area_of_a_circle.lean

@@ -71,7 +71,7 @@ end
 theorem measurable_set_disc : measurable_set (disc r) :=
 by apply measurable_set_lt; apply continuous.measurable; continuity
 
-/-- The area of a disc with radius `r` is `π * r ^ 2`. -/
+/-- **Area of a Circle**: The area of a disc with radius `r` is `π * r ^ 2`. -/
 theorem area_disc : volume (disc r) = nnreal.pi * r ^ 2 :=
 begin
   let f := λ x, sqrt (r ^ 2 - x ^ 2),

archive/arithcc.lean

@@ -281,7 +281,7 @@ begin
   rwa if_neg (ne_of_lt hr) at h
 end
 
-/-- The main theorem on compiler correctness.
+/-- The main **compiler correctness theorem**.
 
 Unlike Theorem 1 in the paper, both `map` and the assumption on `t` are explicit.
 -/

archive/sensitivity.lean

@@ -383,6 +383,7 @@ begin
   linarith
 end
 
+/-- **Huang sensitivity theorem** also known as the **Huang degree theorem** -/
 theorem huang_degree_theorem (H : set (Q (m + 1))) (hH : Card H ≥ 2^m + 1) :
   ∃ q, q ∈ H ∧ √(m + 1) ≤ Card (H ∩ q.adjacent) :=
 begin

counterexamples/girard.lean

@@ -24,7 +24,7 @@ Based on Watkins' LF implementation of Hurkens' simplification of Girard's parad
 * `girard`: there are no Girard universes.
 -/
 
-/-- Girard's paradox: there are no universes `u` such that `Type u : Type u`.
+/-- **Girard's paradox**: there are no universes `u` such that `Type u : Type u`.
 Since we can't actually change the type of Lean's `Π` operator, we assume the existence of
 `pi`, `lam`, `app` and the `beta` rule equivalent to the `Π` and `app` constructors of type theory.
 -/

docs/100.yaml

@@ -59,15 +59,13 @@
   links :
     mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/16_abel_ruffini.lean
 17:
-  title  : De Moivre’s Theorem
+  title  : De Moivre’s Formula
   decl   : complex.cos_add_sin_mul_I_pow
   author : Abhimanyu Pallavi Sudhir
 18:
   title  : Liouville’s Theorem and the Construction of Transcendental Numbers
   author : Jujian Zhang
-  links  :
-    result: https://github.com/jjaassoonn/transcendental/blob/master/src/liouville_theorem.lean
-    website: https://jjaassoonn.github.io/transcendental/
+  decl   :  liouville.transcendental
 19:
   title  : Four Squares Theorem
   decl   : nat.sum_four_squares
@@ -87,7 +85,7 @@
   decl   : pythagorean_triple.classification
   author : Paul van Wamelen
 24:
-  title  : The Undecidability of the Continuum Hypothesis
+  title  : The Independence of the Continuum Hypothesis
   author : Jesse Michael Han and Floris van Doorn
   links  :
     result: https://github.com/flypitch/flypitch/blob/master/src/summary.lean
@@ -170,7 +168,7 @@
 50:
   title  : The Number of Platonic Solids
 51:
-  title  : Wilson’s Theorem
+  title  : Wilson’s Lemma
   decl   : zmod.wilsons_lemma
   author : Chris Hughes
 52:

src/algebra/euclidean_domain.lean

@@ -314,7 +314,7 @@ gcd.induction r r' (by intros; simpa only [xgcd_zero_left]) $ λ x y h IH s t s'
     mod_eq_sub_mul_div]
 end
 
-/-- An explicit version of Bézout's lemma for Euclidean domains. -/
+/-- An explicit version of **Bézout's lemma** for Euclidean domains. -/
 theorem gcd_eq_gcd_ab (a b : R) : (gcd a b : R) = a * gcd_a a b + b * gcd_b a b :=
 by have := @xgcd_aux_P _ _ _ a b a b 1 0 0 1
   (by rw [P, mul_one, mul_zero, add_zero]) (by rw [P, mul_one, mul_zero, zero_add]);

src/algebra/ordered_group.lean

@@ -820,6 +820,9 @@ end
 lemma max_sub_min_eq_abs (a b : α) : max a b - min a b = abs (b - a) :=
 by { rw abs_sub_comm, exact max_sub_min_eq_abs' _ _ }
 
+/--
+The **triangle inequality** in `linear_ordered_add_comm_group`s.
+-/
 lemma abs_add (a b : α) : abs (a + b) ≤ abs a + abs b :=
 abs_le.2 ⟨(neg_add (abs a) (abs b)).symm ▸
   add_le_add (neg_le.2 $ neg_le_abs_self _) (neg_le.2 $ neg_le_abs_self _),

src/analysis/calculus/lhopital.lean

@@ -22,6 +22,10 @@ allowing it to be any filter on `ℝ`.
 Each statement is available in a `has_deriv_at` form and a `deriv` form, which
 is denoted by each statement being in either the `has_deriv_at` or the `deriv`
 namespace.
+
+## Tags
+
+L'Hôpital's rule, L'Hopital's rule
 -/
 
 open filter set
@@ -364,7 +368,7 @@ begin
           lhopital_zero_nhds_right hff'.2 hgg'.2 hg'.2 hfa.2 hga.2 hdiv.2⟩
 end
 
-/-- L'Hôpital's rule for approaching a real, `has_deriv_at` version -/
+/-- **L'Hôpital's rule** for approaching a real, `has_deriv_at` version -/
 theorem lhopital_zero_nhds
   (hff' : ∀ᶠ x in 𝓝 a, has_deriv_at f (f' x) x)
   (hgg' : ∀ᶠ x in 𝓝 a, has_deriv_at g (g' x) x)
@@ -430,7 +434,7 @@ end has_deriv_at
 
 namespace deriv
 
-/-- L'Hôpital's rule for approaching a real from the right, `deriv` version -/
+/-- **L'Hôpital's rule** for approaching a real from the right, `deriv` version -/
 theorem lhopital_zero_nhds_right
   (hdf : ∀ᶠ x in 𝓝[Ioi a] a, differentiable_at ℝ f x)
   (hg' : ∀ᶠ x in 𝓝[Ioi a] a, deriv g x ≠ 0)
@@ -448,7 +452,7 @@ begin
   exact has_deriv_at.lhopital_zero_nhds_right hdf' hdg' hg' hfa hga hdiv
 end
 
-/-- L'Hôpital's rule for approaching a real from the left, `deriv` version -/
+/-- **L'Hôpital's rule** for approaching a real from the left, `deriv` version -/
 theorem lhopital_zero_nhds_left
   (hdf : ∀ᶠ x in 𝓝[Iio a] a, differentiable_at ℝ f x)
   (hg' : ∀ᶠ x in 𝓝[Iio a] a, deriv g x ≠ 0)
@@ -466,7 +470,7 @@ begin
   exact has_deriv_at.lhopital_zero_nhds_left hdf' hdg' hg' hfa hga hdiv
 end
 
-/-- L'Hôpital's rule for approaching a real, `deriv` version. This
+/-- **L'Hôpital's rule** for approaching a real, `deriv` version. This
   does not require anything about the situation at `a` -/
 theorem lhopital_zero_nhds'
   (hdf : ∀ᶠ x in 𝓝[univ \ {a}] a, differentiable_at ℝ f x)
@@ -482,7 +486,7 @@ begin
           lhopital_zero_nhds_right hdf.2 hg'.2 hfa.2 hga.2 hdiv.2⟩,
 end
 
-/-- L'Hôpital's rule for approaching a real, `deriv` version -/
+/-- **L'Hôpital's rule** for approaching a real, `deriv` version -/
 theorem lhopital_zero_nhds
   (hdf : ∀ᶠ x in 𝓝 a, differentiable_at ℝ f x)
   (hg' : ∀ᶠ x in 𝓝 a, deriv g x ≠ 0)
@@ -495,7 +499,7 @@ begin
   assumption
 end
 
-/-- L'Hôpital's rule for approaching +∞, `deriv` version -/
+/-- **L'Hôpital's rule** for approaching +∞, `deriv` version -/
 theorem lhopital_zero_at_top
   (hdf : ∀ᶠ (x : ℝ) in at_top, differentiable_at ℝ f x)
   (hg' : ∀ᶠ (x : ℝ) in at_top, deriv g x ≠ 0)
@@ -513,7 +517,7 @@ begin
   exact has_deriv_at.lhopital_zero_at_top hdf' hdg' hg' hftop hgtop hdiv
 end
 
-/-- L'Hôpital's rule for approaching -∞, `deriv` version -/
+/-- **L'Hôpital's rule** for approaching -∞, `deriv` version -/
 theorem lhopital_zero_at_bot
   (hdf : ∀ᶠ (x : ℝ) in at_bot, differentiable_at ℝ f x)
   (hg' : ∀ᶠ (x : ℝ) in at_bot, deriv g x ≠ 0)

src/analysis/calculus/local_extr.lean

@@ -301,22 +301,22 @@ lemma exists_local_extr_Ioo (hab : a < b) (hfc : continuous_on f (Icc a b)) (hfI
 let ⟨c, cmem, hc⟩ := exists_Ioo_extr_on_Icc f hab hfc hfI
 in ⟨c, cmem, hc.is_local_extr $ Icc_mem_nhds cmem.1 cmem.2⟩
 
-/-- Rolle's Theorem `has_deriv_at` version -/
+/-- **Rolle's Theorem** `has_deriv_at` version -/
 lemma exists_has_deriv_at_eq_zero (hab : a < b) (hfc : continuous_on f (Icc a b)) (hfI : f a = f b)
   (hff' : ∀ x ∈ Ioo a b, has_deriv_at f (f' x) x) :
   ∃ c ∈ Ioo a b, f' c = 0 :=
 let ⟨c, cmem, hc⟩ := exists_local_extr_Ioo f hab hfc hfI in
   ⟨c, cmem, hc.has_deriv_at_eq_zero $ hff' c cmem⟩
 
-/-- Rolle's Theorem `deriv` version -/
+/-- **Rolle's Theorem** `deriv` version -/
 lemma exists_deriv_eq_zero (hab : a < b) (hfc : continuous_on f (Icc a b)) (hfI : f a = f b) :
   ∃ c ∈ Ioo a b, deriv f c = 0 :=
 let ⟨c, cmem, hc⟩ := exists_local_extr_Ioo f hab hfc hfI in
   ⟨c, cmem, hc.deriv_eq_zero⟩
 
 variables {f f'} {l : ℝ}
 
-/-- Rolle's Theorem, a version for a function on an open interval: if `f` has derivative `f'`
+/-- **Rolle's Theorem**, a version for a function on an open interval: if `f` has derivative `f'`
 on `(a, b)` and has the same limit `l` at `𝓝[Ioi a] a` and `𝓝[Iio b] b`, then `f' c = 0`
 for some `c ∈ (a, b)`.  -/
 lemma exists_has_deriv_at_eq_zero' (hab : a < b)
@@ -336,9 +336,9 @@ begin
   exact ⟨Ioo a b, Ioo_mem_nhds hc.1 hc.2, extend_from_extends this⟩
 end
 
-/-- Rolle's Theorem, a version for a function on an open interval: if `f` has the same limit `l` at
-`𝓝[Ioi a] a` and `𝓝[Iio b] b`, then `deriv f c = 0` for some `c ∈ (a, b)`. This version does not
-require differentiability of `f` because we define `deriv f c = 0` whenever `f` is not
+/-- **Rolle's Theorem**, a version for a function on an open interval: if `f` has the same limit
+`l` at `𝓝[Ioi a] a` and `𝓝[Iio b] b`, then `deriv f c = 0` for some `c ∈ (a, b)`. This version
+does not require differentiability of `f` because we define `deriv f c = 0` whenever `f` is not
 differentiable at `c`. -/
 lemma exists_deriv_eq_zero' (hab : a < b)
   (hfa : tendsto f (𝓝[Ioi a] a) (𝓝 l)) (hfb : tendsto f (𝓝[Iio b] b) (𝓝 l)) :

src/analysis/calculus/mean_value.lean

@@ -674,7 +674,7 @@ variables (f f' : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : continuous_on f
 
 include hab hfc hff' hgc hgg'
 
-/-- Cauchy's Mean Value Theorem, `has_deriv_at` version. -/
+/-- Cauchy's **Mean Value Theorem**, `has_deriv_at` version. -/
 lemma exists_ratio_has_deriv_at_eq_ratio_slope :
   ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c :=
 begin
@@ -692,7 +692,7 @@ end
 
 omit hfc hgc
 
-/-- Cauchy's Mean Value Theorem, extended `has_deriv_at` version. -/
+/-- Cauchy's **Mean Value Theorem**, extended `has_deriv_at` version. -/
 lemma exists_ratio_has_deriv_at_eq_ratio_slope' {lfa lga lfb lgb : ℝ}
   (hff' : ∀ x ∈ Ioo a b, has_deriv_at f (f' x) x) (hgg' : ∀ x ∈ Ioo a b, has_deriv_at g (g' x) x)
   (hfa : tendsto f (𝓝[Ioi a] a) (𝓝 lfa)) (hga : tendsto g (𝓝[Ioi a] a) (𝓝 lga))
@@ -756,7 +756,7 @@ exists_ratio_has_deriv_at_eq_ratio_slope' _ _ hab _ _
   (λ x hx, ((hdg x hx).differentiable_at $ Ioo_mem_nhds hx.1 hx.2).has_deriv_at)
   hfa hga hfb hgb
 
-/-- Lagrange's Mean Value Theorem, `deriv` version. -/
+/-- Lagrange's **Mean Value Theorem**, `deriv` version. -/
 lemma exists_deriv_eq_slope : ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a) :=
 exists_has_deriv_at_eq_slope f (deriv f) hab hfc
   (λ x hx, ((hfd x hx).differentiable_at $ is_open.mem_nhds is_open_Ioo hx).has_deriv_at)

src/analysis/complex/polynomial.lean

@@ -23,8 +23,8 @@ namespace complex
 /- The following proof uses the method given at
 <https://ncatlab.org/nlab/show/fundamental+theorem+of+algebra#classical_fta_via_advanced_calculus>
 -/
-/-- The fundamental theorem of algebra. Every non constant complex polynomial
-  has a root. -/
+/-- **Fundamental theorem of algebra**: every non constant complex polynomial
+  has a root -/
 lemma exists_root {f : polynomial ℂ} (hf : 0 < degree f) : ∃ z : ℂ, is_root f z :=
 let ⟨z₀, hz₀⟩ := f.exists_forall_norm_le in
 exists.intro z₀ $ classical.by_contradiction $ λ hf0,

src/analysis/convex/cone.lean

@@ -479,7 +479,7 @@ end
 
 end riesz_extension
 
-/-- M. Riesz extension theorem: given a convex cone `s` in a vector space `E`, a submodule `p`,
+/-- M. **Riesz extension theorem**: given a convex cone `s` in a vector space `E`, a submodule `p`,
 and a linear `f : p → ℝ`, assume that `f` is nonnegative on `p ∩ s` and `p + s = E`. Then
 there exists a globally defined linear function `g : E → ℝ` that agrees with `f` on `p`,
 and is nonnegative on `s`. -/
@@ -495,7 +495,7 @@ begin
   { exact λ x hx, hgs ⟨x, _⟩ hx }
 end
 
-/-- Hahn-Banach theorem: if `N : E → ℝ` is a sublinear map, `f` is a linear map
+/-- **Hahn-Banach theorem**: if `N : E → ℝ` is a sublinear map, `f` is a linear map
 defined on a subspace of `E`, and `f x ≤ N x` for all `x` in the domain of `f`,
 then `f` can be extended to the whole space to a linear map `g` such that `g x ≤ N x`
 for all `x`. -/

src/analysis/mean_inequalities.lean

@@ -114,7 +114,7 @@ variables {ι : Type u} (s : finset ι)
 
 namespace real
 
-/-- AM-GM inequality: the geometric mean is less than or equal to the arithmetic mean, weighted
+/-- AM-GM inequality: the **geometric mean is less than or equal to the arithmetic mean**, weighted
 version for real-valued nonnegative functions. -/
 theorem geom_mean_le_arith_mean_weighted (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
   (hw' : ∑ i in s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) :

src/analysis/normed_space/basic.lean

@@ -140,7 +140,7 @@ by simp only [sub_eq_add_neg, dist_add_left, dist_neg_neg]
 @[simp] lemma dist_sub_right (g₁ g₂ h : α) : dist (g₁ - h) (g₂ - h) = dist g₁ g₂ :=
 by simpa only [sub_eq_add_neg] using dist_add_right _ _ _
 
-/-- Triangle inequality for the norm. -/
+/-- **Triangle inequality** for the norm. -/
 lemma norm_add_le (g h : α) : ∥g + h∥ ≤ ∥g∥ + ∥h∥ :=
 by simpa [dist_eq_norm] using dist_triangle g 0 (-h)
 

src/analysis/normed_space/inner_product.lean

@@ -233,7 +233,7 @@ lemma inner_sub_sub_self {x y : F} : ⟪x - y, x - y⟫ = ⟪x, x⟫ - ⟪x, y
 by simp only [inner_sub_left, inner_sub_right]; ring
 
 /--
-Cauchy–Schwarz inequality. This proof follows "Proof 2" on Wikipedia.
+**Cauchy–Schwarz inequality**. This proof follows "Proof 2" on Wikipedia.
 We need this for the `core` structure to prove the triangle inequality below when
 showing the core is a normed group.
 -/

src/analysis/normed_space/mazur_ulam.lean

@@ -105,7 +105,7 @@ Since `f : PE ≃ᵢ PF` sends midpoints to midpoints, it is an affine map.
 We define a conversion to a `continuous_linear_equiv` first, then a conversion to an `affine_map`.
 -/
 
-/-- Mazur-Ulam Theorem: if `f` is an isometric bijection between two normed vector spaces
+/-- **Mazur-Ulam Theorem**: if `f` is an isometric bijection between two normed vector spaces
 over `ℝ` and `f 0 = 0`, then `f` is a linear equivalence. -/
 def to_real_linear_isometry_equiv_of_map_zero (f : E ≃ᵢ F) (h0 : f 0 = 0) :
   E ≃ₗᵢ[ℝ] F :=
@@ -119,7 +119,7 @@ def to_real_linear_isometry_equiv_of_map_zero (f : E ≃ᵢ F) (h0 : f 0 = 0) :
 @[simp] lemma coe_to_real_linear_equiv_of_map_zero_symm (f : E ≃ᵢ F) (h0 : f 0 = 0) :
   ⇑(f.to_real_linear_isometry_equiv_of_map_zero h0).symm = f.symm := rfl
 
-/-- Mazur-Ulam Theorem: if `f` is an isometric bijection between two normed vector spaces
+/-- **Mazur-Ulam Theorem**: if `f` is an isometric bijection between two normed vector spaces
 over `ℝ`, then `x ↦ f x - f 0` is a linear equivalence. -/
 def to_real_linear_isometry_equiv (f : E ≃ᵢ F) : E ≃ₗᵢ[ℝ] F :=
 (f.trans (isometric.add_right (f 0)).symm).to_real_linear_isometry_equiv_of_map_zero

src/analysis/p_series.lean

@@ -211,7 +211,7 @@ by simpa
 lemma real.not_summable_one_div_nat_cast : ¬summable (λ n, 1 / n : ℕ → ℝ) :=
 by simpa only [inv_eq_one_div] using real.not_summable_nat_cast_inv
 
-/-- Harmonic series diverges. -/
+/-- **Divergence of the Harmonic Series** -/
 lemma real.tendsto_sum_range_one_div_nat_succ_at_top :
   tendsto (λ n, ∑ i in finset.range n, (1 / (i + 1) : ℝ)) at_top at_top :=
 begin

src/analysis/specific_limits.lean

@@ -350,6 +350,7 @@ lemma summable_geometric_two' (a : ℝ) : summable (λ n:ℕ, (a / 2) / 2 ^ n) :
 lemma tsum_geometric_two' (a : ℝ) : ∑' n:ℕ, (a / 2) / 2^n = a :=
 (has_sum_geometric_two' a).tsum_eq
 
+/-- **Sum of a Geometric Series** -/
 lemma nnreal.has_sum_geometric {r : ℝ≥0} (hr : r < 1) :
   has_sum (λ n : ℕ, r ^ n) (1 - r)⁻¹ :=
 begin