Theorems · Theorem · number theory
GenContFract.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none
∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K} {n : ℕ},
(GenContFract.of v).TerminatedAt n ↔ GenContFract.IntFractPair.stream v (n + 1) = none- Cited by
- 5 results in Mathlib
- Foundations
- Depth 51 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- DivisionRingstatement and proof · cited by 1,062
- FloorRingstatement and proof · cited by 405
- GenContFract.ofstatement · cited by 53
- GenContFract.IntFractPairstatement and proof · cited by 45
- GenContFract.IntFractPair.streamstatement and proof · cited by 37
- GenContFract.TerminatedAtstatement · cited by 30
- GenContFract.IntFractPair.seq1proof · cited by 5
- GenContFract.of_terminatedAt_iff_intFractPair_seq1_terminatedAtproof · cited by 1
- GenContFract.IntFractPair.get?_seq1_eq_succ_get?_streamproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- GenContFract.of_correctness_of_terminatedAtproof · cited by 3
- GenContFract.of_s_succproof · cited by 1
- GenContFract.terminates_of_ratproof · cited by 1
- GenContFract.of_correctness_of_nth_stream_eq_noneproof · cited by 1
- GenContFract.sub_convs_eqproof · cited by 0