Theorems · Definition · number theory

GenContFract.of

{K : Type u_1} → [inst : DivisionRing K] → [inst_1 : LinearOrder K] → [FloorRing K] → K → GenContFract K

Returns the GenContFract of a value. In fact, the returned gcf is also a ContFract that terminates if and only if v is rational (see Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean). The continued fraction representation of v is given by [⌊v⌋; b₀, b₁, b₂,...], where [b₀; b₁, b₂,...] recursively is the continued fraction representation of 1 / (v - ⌊v⌋). This process stops when the fractional part v - ⌊v⌋ hits 0 at some step. The implementation uses IntFractPair.stream to obtain the partial denominators of the continued fraction. Refer to said function for more details about the computation process.

Defined in

Mathlib.Algebra.ContinuedFractions.Computation.Basic

Cited by

53 results in Mathlib

Foundations

Depth 49 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingLinearOrderFloorRing