convs' — Mathlib

English

The convergents of a generalized continued fraction g are given by convs' = g.h + convs'Aux g.s.

Русский

Сходимые дроби обобщённой дроби g задаются как convs' = g.h + convs'Aux g.s.

LaTeX

$$$convs' (g) = g.h + convs'Aux(g.s)$$$

Lean4

/-- Returns the convergents of `g` by evaluating the fraction described by `g` up to a given
position `n`. For example, `convs' [9; (1, 2), (3, 4), (5, 6)] 2 = 9 + 1 / (2 + 3 / 4)` and
`convs' [9; (1, 2), (3, 4), (5, 6)] 0 = 9`
-/
def convs' (g : GenContFract K) (n : ℕ) : K :=
  g.h + convs'Aux g.s n

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