Theorems · Theorem · number theory

GenContFract.contsAux.eq_def

∀ {K : Type u_2} [inst : DivisionRing K] (g : GenContFract K) (x : ℕ),
  g.contsAux x =
    match x with
    | 0 => { a := 1, b := 0 }
    | 1 => { a := g.h, b := 1 }
    | n.succ.succ =>
      match g.s.get? n with
      | none => g.contsAux (n + 1)
      | some gp => GenContFract.nextConts gp.a gp.b (g.contsAux n) (g.contsAux (n + 1))

Defined in

Mathlib.Algebra.ContinuedFractions.Translations

Cited by

0 results in Mathlib

Foundations

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

Assumes

DivisionRing