Theorems · Theorem · number theory

GenContFract.IntFractPair.nth_stream_fr_nonneg

∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K] {ifp_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some ifp_n → 0 ≤ ifp_n.fr

Shows that the fractional parts of the stream are nonnegative.

Defined in: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Cited by: 3 results in Mathlib
Foundations: Depth 49 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field LinearOrder IsStrictOrderedRing FloorRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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

LinearOrderstatement and proof · cited by 8,572
Fieldstatement and proof · cited by 7,404
IsStrictOrderedRingstatement and proof · cited by 2,490
FloorRingstatement and proof · cited by 405
GenContFract.IntFractPairstatement and proof · cited by 45
GenContFract.IntFractPair.streamstatement and proof · cited by 37
GenContFract.IntFractPair.frstatement · cited by 25
GenContFract.IntFractPair.nth_stream_fr_nonneg_lt_oneproof · cited by 4

Cited by3

Results whose statement or proof uses this declaration.

GenContFract.abs_sub_convs_leproof · cited by 2
GenContFract.IntFractPair.one_le_succ_nth_stream_bproof · cited by 1
GenContFract.sub_convs_eqproof · cited by 0