zeroth_conv'_eq_h

Mathlib.Algebra.ContinuedFractions.Translations

URI: https://scilib.ai/kg/mathlib#GenContFract.zeroth_conv'_eq_h

English

The zeroth convs' equals h.

Русский

Нулевое convs' равно h.

LaTeX

$$$ g.convs' 0 = g.h $$$

Lean4

@[simp]
theorem zeroth_conv'_eq_h : g.convs' 0 = g.h := by simp [convs']

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

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

Разделы

Аффилиация

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