Theorems · Definition · number theory
SimpContFract
(α : Type u_1) → [One α] → Type (max 0 u_1)
A simple continued fraction (scf) is a generalized continued fraction (gcf) whose partial
numerators are equal to one.
$$
h + \dfrac{1}
{b_0 + \dfrac{1}
{b_1 + \dfrac{1}
{b_2 + \dfrac{1}
{b_3 + \dots}}}}
$$
For convenience, one often writes [h; b₀, b₁, b₂,...].
It is encoded as the subtype of gcfs that satisfy GenContFract.IsSimpContFract.
- Defined in
- Mathlib.Algebra.ContinuedFractions.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses no axioms
- Assumes
- One
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- GenContFractproof · cited by 68
- GenContFract.IsSimpContFractproof · cited by 3
Cited by6
Results whose statement or proof uses this declaration.
- SimpContFract.IsContFractstatement and proof · cited by 2
- ContFract.convs_eq_convs'statement · cited by 1
- ContFractproof · cited by 1
- SimpContFract.determinantstatement and proof · cited by 1
- SimpContFract.ofstatement · cited by 1
- SimpContFract.ofIntegerstatement · cited by 0