Theorems · Theorem · number theory

GenContFract.of_correctness_of_nth_stream_eq_none

∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] {v : K} {n : ℕ} [inst_2 : FloorRing K],
  GenContFract.IntFractPair.stream v n = none → v = (GenContFract.of v).convs (n - 1)

The convergent of GenContFract.of v at step n - 1 is exactly v if the IntFractPair.stream of the corresponding continued fraction terminated at step n.

Defined in

Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderFloorRing