Determinant Formula for Simple Continued Fraction

Summary

We derive the so-called determinant formula for SimpContFract: Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1)^(n + 1).

TODO

Generalize this for GenContFract version: Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-a₀) * (-a₁) * .. * (-aₙ₊₁).

References

• https://en.wikipedia.org/wiki/Generalized_continued_fraction#The_determinant_formula

theorem SimpContFract.determinant_aux {K : Type u_1} [Field K] {s : SimpContFract K} {n : ℕ} (hyp : n = 0 ∨ ¬(↑s).TerminatedAt (n - 1)) : ((↑s).contsAux n).a * ((↑s).contsAux (n + 1)).b - ((↑s).contsAux n).b * ((↑s).contsAux (n + 1)).a = (-1) ^ n

theorem SimpContFract.determinant {K : Type u_1} [Field K] {s : SimpContFract K} {n : ℕ} (not_terminatedAt_n : ¬(↑s).TerminatedAt n) : (↑s).nums n * (↑s).dens (n + 1) - (↑s).dens n * (↑s).nums (n + 1) = (-1) ^ (n + 1)

The determinant formula Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1)^(n + 1).