conv_eq_num_div_den

Mathlib.Algebra.ContinuedFractions.Translations

URI: https://scilib.ai/kg/mathlib#GenContFract.conv_eq_num_div_den

English

The nth convergent equals nums n divided by dens n.

Русский

f(n)-й сходящийся равен nums(n) делить на dens(n).

LaTeX

$$$g.convs n = \\dfrac{g.nums n}{g.dens n}$$$

Lean4

theorem conv_eq_num_div_den : g.convs n = g.nums n / g.dens n :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru