conv_eq_conts_a_div_conts_b

Mathlib.Algebra.ContinuedFractions.Translations

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

English

The nth convergent equals (conts n).a divided by (conts n).b.

Русский

n-й сходящийся равен (conts n).a делённому на (conts n).b.

LaTeX

$$$g.convs n = \\dfrac{(g.conts n).a}{(g.conts n).b}$$$

Lean4

theorem conv_eq_conts_a_div_conts_b : g.convs n = (g.conts n).a / (g.conts n).b :=
  rfl

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

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

Разделы

Аффилиация

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