Theorems · Theorem · number theory

GenContFract.second_contAux_eq

∀ {K : Type u_1} {g : GenContFract K} [inst : DivisionRing K] {gp : GenContFract.Pair K},
  g.s.get? 0 = some gp → g.contsAux 2 = { a := gp.b * g.h + gp.a, b := gp.b }

Defined in

Mathlib.Algebra.ContinuedFractions.Translations

Cited by

1 results in Mathlib

Foundations

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

Assumes

DivisionRing