doc(algebra/continued_fractions/*): TeXify docstrings (#18459)

MichaelStollBayreuth · MichaelStollBayreuth · commit 2738d2ca56cb · 2023-02-17T18:50:51.000Z
Improve readability of continued fractions in the docstrings by randering them via LaTeX.
diff --git a/src/algebra/continued_fractions/basic.lean b/src/algebra/continued_fractions/basic.lean
@@ -80,17 +80,13 @@ variable (α)
 
 /--
 A *generalised continued fraction* (gcf) is a potentially infinite expression of the form
-
-                                a₀
-                h + ---------------------------
-                                  a₁
-                      b₀ + --------------------
-                                    a₂
-                            b₁ + --------------
-                                        a₃
-                                  b₂ + --------
-                                      b₃ + ...
-
+$$
+  h + \dfrac{a_0}
+            {b_0 + \dfrac{a_1}
+                         {b_1 + \dfrac{a_2}
+                                      {b_2 + \dfrac{a_3}
+                                                   {b_3 + \dots}}}}
+$$
 where `h` is called the *head term* or *integer part*, the `aᵢ` are called the
 *partial numerators* and the `bᵢ` the *partial denominators* of the gcf.
 We store the sequence of partial numerators and denominators in a sequence of
@@ -150,17 +146,13 @@ end generalized_continued_fraction
 /--
 A generalized continued fraction is a *simple continued fraction* if all partial numerators are
 equal to one.
-
-                                1
-                h + ---------------------------
-                                  1
-                      b₀ + --------------------
-                                    1
-                            b₁ + --------------
-                                        1
-                                  b₂ + --------
-                                      b₃ + ...
-
+$$
+  h + \dfrac{1}
+            {b_0 + \dfrac{1}
+                         {b_1 + \dfrac{1}
+                                      {b_2 + \dfrac{1}
+                                                   {b_3 + \dots}}}}
+$$
 -/
 def generalized_continued_fraction.is_simple_continued_fraction
   (g : generalized_continued_fraction α) [has_one α] : Prop :=
@@ -170,17 +162,13 @@ variable (α)
 /--
 A *simple continued fraction* (scf) is a generalized continued fraction (gcf) whose partial
 numerators are equal to one.
-
-                                1
-                h + ---------------------------
-                                  1
-                      b₀ + --------------------
-                                    1
-                            b₁ + --------------
-                                        1
-                                  b₂ + --------
-                                      b₃ + ...
-
+$$
+  h + \dfrac{1}
+            {b_0 + \dfrac{1}
+                         {b_1 + \dfrac{1}
+                                      {b_2 + \dfrac{1}
+                                                   {b_3 + \dots}}}}
+$$
 For convenience, one often writes `[h; b₀, b₁, b₂,...]`.
 It is encoded as the subtype of gcfs that satisfy
 `generalized_continued_fraction.is_simple_continued_fraction`.
diff --git a/src/algebra/continued_fractions/computation/approximation_corollaries.lean b/src/algebra/continued_fractions/computation/approximation_corollaries.lean
@@ -70,7 +70,7 @@ lemma of_convergents_eq_convergents' :
 The recurrence relation for the `convergents` of the continued fraction expansion
 of an element `v` of `K` in terms of the convergents of the inverse of its fractional part.
 -/
-lemma convergents_succ (n : ℕ):
+lemma convergents_succ (n : ℕ) :
   (of v).convergents (n + 1) = ⌊v⌋ + 1 / (of (int.fract v)⁻¹).convergents n :=
 by rw [of_convergents_eq_convergents', convergents'_succ, of_convergents_eq_convergents']
 
diff --git a/src/algebra/continued_fractions/convergents_equiv.lean b/src/algebra/continued_fractions/convergents_equiv.lean
@@ -18,17 +18,13 @@ direct evaluation (`convergents'`)) for `gcf`s on linear ordered fields. We foll
 [hardy2008introduction], Chapter 10. Here's a sketch:
 
 Let `c` be a continued fraction `[h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...]`, visually:
-
-                                a₀
-                h + ---------------------------
-                                  a₁
-                      b₀ + --------------------
-                                    a₂
-                            b₁ + --------------
-                                        a₃
-                                  b₂ + --------
-                                      b₃ + ...
-
+$$
+  c = h + \dfrac{a_0}
+                {b_0 + \dfrac{a_1}
+                             {b_1 + \dfrac{a_2}
+                                          {b_2 + \dfrac{a_3}
+                                                       {b_3 + \dots}}}}
+$$
 One can compute the convergents of `c` in two ways:
 1. Directly evaluating the fraction described by `c` up to a given `n` (`convergents'`)
 2. Using the recurrence (`convergents`):
