Theorems · Theorem · number theory
GenContFract.of_correctness_of_terminatedAt
∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] {v : K} {n : ℕ} [inst_2 : FloorRing K],
(GenContFract.of v).TerminatedAt n → v = (GenContFract.of v).convs nIf GenContFract.of v terminated at step n, then the nth convergent is exactly v.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FieldLinearOrderFloorRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- FloorRingstatement and proof · cited by 405
- GenContFract.ofstatement and proof · cited by 53
- GenContFract.IntFractPair.streamproof · cited by 37
- GenContFract.TerminatedAtstatement and proof · cited by 30
- GenContFract.convsstatement · cited by 22
- GenContFract.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_noneproof · cited by 5
- GenContFract.of_correctness_of_nth_stream_eq_noneproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- GenContFract.of_convergence_epsilonproof · cited by 1
- GenContFract.of_correctness_of_terminatesproof · cited by 1
- GenContFract.of_correctness_atTop_of_terminatesproof · cited by 0