Theorems · Theorem · number theory
GenContFract.partNum_eq_s_a
∀ {α : Type u_1} {g : GenContFract α} {n : ℕ} {gp : GenContFract.Pair α},
g.s.get? n = some gp → g.partNums.get? n = some gp.a- Cited by
- 5 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Stream'.Seq.get?statement and proof · cited by 122
- GenContFract.Pairstatement and proof · cited by 85
- GenContFractstatement and proof · cited by 68
- GenContFract.sstatement and proof · cited by 57
- GenContFract.Pair.astatement and proof · cited by 43
- Stream'.Seq.map_get?proof · cited by 14
- GenContFract.partNumsstatement · cited by 7
Cited by5
Results whose statement or proof uses this declaration.
- GenContFract.fib_le_of_contsAux_bproof · cited by 4
- GenContFract.abs_sub_convs_leproof · cited by 2
- GenContFract.le_of_succ_succ_get?_contsAux_bproof · cited by 1
- ContFract.convs_eq_convs'proof · cited by 1
- SimpContFract.determinantproof · cited by 1