Theorems · Theorem · number theory

GenContFract.sub_convs_eq

∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K] {ifp : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some ifp →
    have g := GenContFract.of v;
    have B := (g.contsAux (n + 1)).b;
    have pB := (g.contsAux n).b;
    v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

This lemma follows from the finite correctness proof, the determinant equality, and by simplifying the difference.

Defined in

Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingFloorRing