Theorems · Definition · number theory
GenContFract.partDens
{α : Type u_1} → GenContFract α → Stream'.Seq αReturns the sequence of partial denominators bᵢ of g.
- Defined in
- Mathlib.Algebra.ContinuedFractions.Basic
- Cited by
- 13 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.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Stream'.Seqstatement · cited by 226
- GenContFractstatement and proof · cited by 68
- GenContFract.sproof · cited by 57
- GenContFract.Pair.bproof · cited by 51
- Stream'.Seq.mapproof · cited by 39
Cited by15
Results whose statement or proof uses this declaration.
- GenContFract.of_one_le_get?_partDenstatement and proof · cited by 4
- GenContFract.exists_s_b_of_partDenstatement and proof · cited by 3
- GenContFract.partDen_eq_s_bstatement · cited by 3
- GenContFract.le_of_succ_get?_denstatement and proof · cited by 2
- SimpContFract.IsContFractproof · cited by 2
- GenContFract.succ_nth_conv_eq_squashGCF_nth_convstatement and proof · cited by 1
- GenContFract.terminatedAt_iff_partDen_nonestatement and proof · cited by 1
- GenContFract.le_of_succ_succ_get?_contsAux_bstatement and proof · cited by 1
- GenContFract.convs_eq_convs'proof · cited by 1
- GenContFract.partDen_none_iff_s_nonestatement · cited by 1
- GenContFract.abs_sub_convergents_le'statement and proof · cited by 0
- SimpContFract.of_isContFractproof · cited by 0