Theorems · Definition · number theory
GenContFract.TerminatedAt
{α : Type u_1} → GenContFract α → ℕ → PropA gcf terminated at position n if its sequence terminates at position n.
- Defined in
- Mathlib.Algebra.ContinuedFractions.Basic
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- GenContFractstatement and proof · cited by 68
- GenContFract.sproof · cited by 57
- Stream'.Seq.TerminatedAtproof · cited by 26
Cited by30
Results whose statement or proof uses this declaration.
- GenContFract.terminated_stablestatement and proof · cited by 6
- GenContFract.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_nonestatement · cited by 5
- GenContFract.fib_le_of_contsAux_bstatement and proof · cited by 4
- GenContFract.terminatedAt_iff_s_nonestatement · cited by 4
- GenContFract.convs_stable_of_terminatedstatement and proof · cited by 4
- GenContFract.of_correctness_of_terminatedAtstatement and proof · cited by 3
- GenContFract.dens_stable_of_terminatedstatement and proof · cited by 3
- GenContFract.nums_stable_of_terminatedstatement and proof · cited by 2
- GenContFract.squashGCF_eq_self_of_terminatedstatement and proof · cited by 2
- GenContFract.abs_sub_convs_lestatement and proof · cited by 2
- GenContFract.contsAux_stable_of_terminatedstatement and proof · cited by 2
- GenContFract.contsAux_stable_step_of_terminatedstatement and proof · cited by 2