Theorems · Theorem · number theory

GenContFract.of_s_tail

∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K)
  [IsStrictOrderedRing K], (GenContFract.of v).s.tail = (GenContFract.of (Int.fract v)⁻¹).s

This expresses the tail of the coefficient sequence of the GenContFract.of an element v of K as the coefficient sequence of that of the inverse of the fractional part of v.

Defined in

Mathlib.Algebra.ContinuedFractions.Computation.Translations

Cited by

1 results in Mathlib

Foundations

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

Assumes

DivisionRingLinearOrderFloorRingIsStrictOrderedRing