Mathlib Map

Theorems · Theorem · number theory

GenContFract.of_s_of_int

∀ (K : Type u_1) [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] [IsStrictOrderedRing K]
  (a : ℤ), (GenContFract.of ↑a).s = Stream'.Seq.nil

If a is an integer, then the coefficient sequence of its continued fraction is empty.

Defined in
Mathlib.Algebra.ContinuedFractions.Computation.Translations
Cited by
2 results in Mathlib
Foundations
Depth 53 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
DivisionRingLinearOrderFloorRingIsStrictOrderedRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

GenContFract.of_s_succ · cited by 1GenContFract.of_s_succGenContFract.convs'_of_int · cited by 1GenContFract.convs'_of_intLinearOrder · cited by 8572LinearOrderIsStrictOrderedRing · cited by 2490IsStrictOrderedRingDivisionRing · cited by 1062DivisionRingSubtype.prop · cited by 505Subtype.propFloorRing · cited by 405FloorRingStream'.Seq · cited by 226Stream'.SeqStream'.Seq.get? · cited by 122Seq.get?GenContFract.Pair · cited by 85GenContFract.PairStream'.Seq.nil · cited by 72Seq.nilGenContFract.s · cited by 57GenContFract.sGenContFract.of · cited by 53GenContFract.ofGenContFract.IntFractPair · cited by 45GenContFract.IntFractPairStream'.Seq.ext · cited by 20Seq.extGenContFract.IntFractPair.b · cited by 16IntFractPair.bStream'.Seq.get?_nil · cited by 3Seq.get?_nilGenContFract.of_s_of_intCITED BYCITES

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.