Determinant Formula for Generalized Continued Fraction

We derive the so-called determinant formula for GenContFract: Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-a₀) * (-a₁) * .. * (-aₙ).

References

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

theorem GenContFract.determinant {K : Type u_1} [Field K] {g : GenContFract K} {n : ℕ} : g.nums n * g.dens (n + 1) - g.dens n * g.nums (n + 1) = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

The determinant formula Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-a₀) * (-a₁) * .. * (-aₙ).

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) for SimpContFract.