convs_succ — Mathlib

English

The two notions of convergents, convs and convs', coincide for the standard GenContFract construction.

Русский

Две концепции множителей сходящихся дробей convs и convs' совпадают для стандартного построения GenContFract.

LaTeX

$$$(of v).convs = (of v).convs'$$$

Lean4

/-- The recurrence relation for the convergents of the continued fraction expansion
of an element `v` of `K` in terms of the convergents of the inverse of its fractional part.
-/
theorem convs_succ (n : ℕ) : (of v).convs (n + 1) = ⌊v⌋ + 1 / (of (Int.fract v)⁻¹).convs n := by
  rw [of_convs_eq_convs', convs'_succ, of_convs_eq_convs']

Похожие утверждения