Theorems · Definition · number theory

GenContFract.IntFractPair.seq1

{K : Type u_1} →
  [inst : DivisionRing K] → [inst_1 : LinearOrder K] → [FloorRing K] → K → Stream'.Seq1 (GenContFract.IntFractPair K)

Uses IntFractPair.stream to create a sequence with head (i.e. seq1) of integer and fractional parts of a value v. The first value of IntFractPair.stream is never none, so we can safely extract it and put the tail of the stream in the sequence part. This is just an intermediate representation and users should not (need to) directly interact with it. The setup of rewriting/simplification lemmas that make the definitions easy to use is done in Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean.

Defined in

Mathlib.Algebra.ContinuedFractions.Computation.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

DivisionRingLinearOrderFloorRing