Theorems · Inductive type · number theory

GenContFract

Type u_1 → Type u_1

A generalised continued fraction (gcf) is a potentially infinite expression of the form $$ h + \dfrac{a_0} {b_0 + \dfrac{a_1} {b_1 + \dfrac{a_2} {b_2 + \dfrac{a_3} {b_3 + \dots}}}} $$ where h is called the head term or integer part, the aᵢ are called the partial numerators and the bᵢ the partial denominators of the gcf. We store the sequence of partial numerators and denominators in a sequence of GenContFract.Pairs s. For convenience, one often writes [h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...].

Defined in

Mathlib.Algebra.ContinuedFractions.Basic

Cited by

68 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms