feat(algebra/continued_fractions) add determinant formula and approxi…

…mations for error term (#6461)

src/algebra/continued_fractions/basic.lean

@@ -40,12 +40,13 @@ numerics, number theory, approximations, fractions
 
 -- Fix a carrier `α`.
 variable (α : Type*)
+/-!### Definitions-/
 
 /-- We collect a partial numerator `aᵢ` and partial denominator `bᵢ` in a pair `⟨aᵢ,bᵢ⟩`. -/
 @[derive inhabited]
 protected structure generalized_continued_fraction.pair := (a : α) (b : α)
 
-/- Interlude: define some expected coercions and instances. -/
+/-! Interlude: define some expected coercions and instances. -/
 namespace generalized_continued_fraction.pair
 open generalized_continued_fraction as gcf
 
@@ -60,7 +61,6 @@ def map {β : Type*} (f : α → β) (gp : gcf.pair α) : gcf.pair β :=
 ⟨f gp.a, f gp.b⟩
 
 section coe
-/-! Interlude: define some expected coercions. -/
 /- Fix another type `β` which we will convert to. -/
 variables {β : Type*} [has_coe α β]
 
@@ -227,7 +227,7 @@ def continued_fraction [has_one α] [has_zero α] [has_lt α] :=
 
 variable {α}
 
-/- Interlude: define some expected coercions. -/
+/-! Interlude: define some expected coercions. -/
 namespace continued_fraction
 open generalized_continued_fraction as gcf
 open simple_continued_fraction as scf
@@ -253,19 +253,21 @@ lemma coe_to_generalized_continued_fraction {c : cf α} : (↑c : gcf α) = c.va
 
 end continued_fraction
 
-/-
+namespace generalized_continued_fraction
+/-!
+### Computation of Convergents
+
 We now define how to compute the convergents of a gcf. There are two standard ways to do this:
 directly evaluating the (infinite) fraction described by the gcf or using a recurrence relation.
 For (r)cfs, these computations are equivalent as shown in
 `algebra.continued_fractions.convergents_equiv`.
 -/
-namespace generalized_continued_fraction
 open generalized_continued_fraction as gcf
 
 -- Fix a division ring for the computations.
 variables {K : Type*} [division_ring K]
 
-/-
+/-!
 We start with the definition of the recurrence relation. Given a gcf `g`, for all `n ≥ 1`, we define
 - `A₋₁ = 1,  A₀ = h,  Aₙ = bₙ₋₁ * Aₙ₋₁ + aₙ₋₁ * Aₙ₋₂`, and
 - `B₋₁ = 0,  B₀ = 1,  Bₙ = bₙ₋₁ * Bₙ₋₁ + aₙ₋₁ * Bₙ₋₂`.