Translations

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

Statistics

Metric	Count
Definitions	0
Theorems conv_eq_conts_a_div_conts_b, conv_eq_num_div_den, convs'Aux_succ_none, convs'Aux_succ_some, den_eq_conts_b, exists_conts_a_of_num, exists_conts_b_of_den, exists_s_a_of_partNum, exists_s_b_of_partDen, first_contAux_eq_h_one, first_cont_eq, first_den_eq, first_num_eq, nth_cont_eq_succ_nth_contAux, num_eq_conts_a, partDen_eq_s_b, partDen_none_iff_s_none, partNum_eq_s_a, partNum_none_iff_s_none, second_contAux_eq, terminatedAt_iff_partDen_none, terminatedAt_iff_partNum_none, terminatedAt_iff_s_none, terminatedAt_iff_s_terminatedAt, zeroth_contAux_eq_one_zero, zeroth_cont_eq_h_one, zeroth_conv'Aux_eq_zero, zeroth_conv'_eq_h, zeroth_conv_eq_h, zeroth_den_eq_one, zeroth_num_eq_h	31
Total	31

GenContFract

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conv_eq_conts_a_div_conts_b 📖	mathematical	—	convs DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Pair.a conts Pair.b	—	—
conv_eq_num_div_den 📖	mathematical	—	convs DivInvMonoid.toDiv DivisionRing.toDivInvMonoid nums dens	—	—
convs'Aux_succ_none 📖	mathematical	Stream'.Seq.head Pair	convs'Aux MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing	—	—
convs'Aux_succ_some 📖	mathematical	Stream'.Seq.head Pair	convs'Aux DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Pair.a Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Pair.b Stream'.Seq.tail	—	—
den_eq_conts_b 📖	mathematical	—	dens Pair.b conts	—	—
exists_conts_a_of_num 📖	mathematical	nums	conts Pair.a	—	—
exists_conts_b_of_den 📖	mathematical	dens	conts Pair.b	—	—
exists_s_a_of_partNum 📖	mathematical	Stream'.Seq.get? partNums	Pair s Pair.a	—	Stream'.Seq.map_get?
exists_s_b_of_partDen 📖	mathematical	Stream'.Seq.get? partDens	Pair s Pair.b	—	Stream'.Seq.map_get?
first_contAux_eq_h_one 📖	mathematical	—	contsAux h AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing	—	—
first_cont_eq 📖	mathematical	Stream'.Seq.get? Pair s	conts Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Distrib.toMul Pair.b h Pair.a	—	second_contAux_eq
first_den_eq 📖	mathematical	Stream'.Seq.get? Pair s	dens Pair.b	—	first_cont_eq
first_num_eq 📖	mathematical	Stream'.Seq.get? Pair s	nums Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Distrib.toMul Pair.b h Pair.a	—	first_cont_eq
nth_cont_eq_succ_nth_contAux 📖	mathematical	—	conts contsAux	—	—
num_eq_conts_a 📖	mathematical	—	nums Pair.a conts	—	—
partDen_eq_s_b 📖	mathematical	Stream'.Seq.get? Pair s	partDens Pair.b	—	Stream'.Seq.map_get?
partDen_none_iff_s_none 📖	mathematical	—	Stream'.Seq.get? partDens Pair s	—	Stream'.Seq.map_get?
partNum_eq_s_a 📖	mathematical	Stream'.Seq.get? Pair s	partNums Pair.a	—	Stream'.Seq.map_get?
partNum_none_iff_s_none 📖	mathematical	—	Stream'.Seq.get? partNums Pair s	—	Stream'.Seq.map_get?
second_contAux_eq 📖	mathematical	Stream'.Seq.get? Pair s	contsAux Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Distrib.toMul Pair.b h Pair.a	—	mul_one MulZeroClass.mul_zero add_zero
terminatedAt_iff_partDen_none 📖	mathematical	—	TerminatedAt Stream'.Seq.get? partDens	—	terminatedAt_iff_s_none partDen_none_iff_s_none
terminatedAt_iff_partNum_none 📖	mathematical	—	TerminatedAt Stream'.Seq.get? partNums	—	terminatedAt_iff_s_none partNum_none_iff_s_none
terminatedAt_iff_s_none 📖	mathematical	—	TerminatedAt Stream'.Seq.get? Pair s	—	—
terminatedAt_iff_s_terminatedAt 📖	mathematical	—	TerminatedAt Stream'.Seq.TerminatedAt Pair s	—	—
zeroth_contAux_eq_one_zero 📖	mathematical	—	contsAux AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
zeroth_cont_eq_h_one 📖	mathematical	—	conts h AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing	—	—
zeroth_conv'Aux_eq_zero 📖	mathematical	—	convs'Aux MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing	—	—
zeroth_conv'_eq_h 📖	mathematical	—	convs' h	—	add_zero
zeroth_conv_eq_h 📖	mathematical	—	convs h	—	div_one
zeroth_den_eq_one 📖	mathematical	—	dens AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing	—	—
zeroth_num_eq_h 📖	mathematical	—	nums h	—	—

---

← Back to Index