Theorems · Theorem · number theory

GenContFract.determinant

∀ {K : Type u_1} [inst : 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ₙ).

Defined in

Mathlib.Algebra.ContinuedFractions.Determinant

Cited by

1 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Field