Theorems · Theorem · number theory

GenContFract.nums_recurrence

∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K] {gp : GenContFract.Pair K} {ppredA predA : K},
  g.s.get? (n + 1) = some gp →
    g.nums n = ppredA → g.nums (n + 1) = predA → g.nums (n + 2) = gp.b * predA + gp.a * ppredA

Shows that Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂.

Defined in

Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence

Cited by

0 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Quot.sound

Assumes

DivisionRing