ContinuantsRecurrence

📁 Source: Mathlib/Algebra/ContinuedFractions/ContinuantsRecurrence.lean

Statistics

Metric	Count
Definitions	0
Theorems contsAux_recurrence, conts_recurrence, conts_recurrenceAux, dens_recurrence, nums_recurrence	5
Total	5

GenContFract

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contsAux_recurrence 📖	mathematical	Stream'.Seq.get? Pair s contsAux	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Distrib.toMul Pair.b Pair.a	—	—
conts_recurrence 📖	mathematical	Stream'.Seq.get? Pair s conts	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Distrib.toMul Pair.b Pair.a	—	conts_recurrenceAux nth_cont_eq_succ_nth_contAux
conts_recurrenceAux 📖	mathematical	Stream'.Seq.get? Pair s contsAux	conts Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Distrib.toMul Pair.b Pair.a	—	contsAux_recurrence
dens_recurrence 📖	mathematical	Stream'.Seq.get? Pair s dens	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Distrib.toMul Pair.b Pair.a	—	exists_conts_b_of_den den_eq_conts_b conts_recurrence
nums_recurrence 📖	mathematical	Stream'.Seq.get? Pair s nums	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Distrib.toMul Pair.b Pair.a	—	exists_conts_a_of_num num_eq_conts_a conts_recurrence

---

← Back to Index