Theorems · Definition · number theory
GenContFract.IntFractPair.b
{K : Type u_1} → GenContFract.IntFractPair K → ℤ- Cited by
- 16 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- GenContFract.IntFractPairstatement and proof · cited by 45
Cited by18
Results whose statement or proof uses this declaration.
- GenContFract.ofproof · cited by 53
- GenContFract.IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_somestatement and proof · cited by 4
- GenContFract.IntFractPair.mapFrproof · cited by 4
- GenContFract.of_one_le_get?_partDenproof · cited by 4
- GenContFract.get?_of_eq_some_of_succ_get?_intFractPair_streamstatement and proof · cited by 3
- GenContFract.of_partNum_eq_one_and_exists_int_partDen_eqproof · cited by 3
- GenContFract.abs_sub_convs_leproof · cited by 2
- GenContFract.of_s_head_auxstatement and proof · cited by 2
- GenContFract.of_s_of_intproof · cited by 2
- GenContFract.get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zerostatement · cited by 1
- GenContFract.coe_of_s_get?_rat_eqproof · cited by 1
- GenContFract.IntFractPair.coe_stream_nth_rat_eqproof · cited by 1