Theorems · Theorem · number theory

GenContFract.succ_nth_conv_eq_squashGCF_nth_conv

∀ {K : Type u_1} {n : ℕ} {g : GenContFract K} [inst : Field K],
  (∀ {b : K}, g.partDens.get? n = some b → b ≠ 0) → g.convs (n + 1) = (g.squashGCF n).convs n

The convergents coincide in the expected way at the squashed position if the partial denominator at the squashed position is not zero.

Defined in

Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Cited by

1 results in Mathlib

Foundations

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

Assumes

Field