Theorems · Theorem · number theory

GenContFract.contsAux_recurrence

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

Defined in

Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence

Cited by

8 results in Mathlib

Foundations

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

Assumes

DivisionRing