nth_cont_eq_succ_nth_contAux

Mathlib.Algebra.ContinuedFractions.Translations

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

English

For all g and n, the n-th continuation equals the (n+1)-st auxiliary continuation: conts n = contsAux (n+1).

Русский

Для всех g и n выполняется: conts(n) = contsAux(n+1).

LaTeX

$$$$ g.conts n = g.contsAux (n + 1). $$$$

Lean4

theorem nth_cont_eq_succ_nth_contAux : g.conts n = g.contsAux (n + 1) :=
  rfl

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

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

Разделы

Аффилиация

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