zeroth_contAux_eq_one_zero

Mathlib.Algebra.ContinuedFractions.Translations

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

English

The zeroth contAux is the pair (1,0).

Русский

Нулевой contAux равен паре (1,0).

LaTeX

$$$g.contsAux 0 = \\langle 1, 0 \\rangle$$$

Lean4

@[simp]
theorem zeroth_contAux_eq_one_zero : g.contsAux 0 = ⟨1, 0⟩ :=
  rfl

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

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

Разделы

Аффилиация

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