Documentation Verification Report

ConvergentsEquiv

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

Statistics

Metric	Count
Definitions `squashGCF`, `squashSeq`	2
Theorems `convs_eq_convs'`, `contsAux_eq_contsAux_squashGCF_of_le`, `convs_eq_convs'`, `squashGCF_eq_self_of_terminated`, `squashGCF_nth_of_lt`, `squashSeq_eq_self_of_terminated`, `squashSeq_nth_of_lt`, `squashSeq_nth_of_not_terminated`, `squashSeq_succ_n_tail_eq_squashSeq_tail_n`, `succ_nth_conv'_eq_squashGCF_nth_conv'`, `succ_nth_conv_eq_squashGCF_nth_conv`, `succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq`	12
Total	14

ContFract

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convs_eq_convs'` 📖	mathematical	—	`GenContFract.convs` `Field.toDivisionRing` `GenContFract` `GenContFract.IsSimpContFract` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `SimpContFract` `SimpContFract.IsContFract` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `GenContFract.convs'`	—	`Stream'.ext` `GenContFract.convs_eq_convs'` `LT.lt.trans_le` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Eq.le` `GenContFract.partNum_eq_s_a` `GenContFract.partDen_eq_s_b`

GenContFract

Definitions

Name	Category	Theorems
`squashGCF` 📖	CompOp	5 math math: `succ_nth_conv_eq_squashGCF_nth_conv`, `contsAux_eq_contsAux_squashGCF_of_le`, `succ_nth_conv'_eq_squashGCF_nth_conv'`, `squashGCF_eq_self_of_terminated`, `squashGCF_nth_of_lt`
`squashSeq` 📖	CompOp	5 math math: `squashSeq_succ_n_tail_eq_squashSeq_tail_n`, `squashSeq_nth_of_lt`, `succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq`, `squashSeq_eq_self_of_terminated`, `squashSeq_nth_of_not_terminated`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contsAux_eq_contsAux_squashGCF_of_le` 📖	mathematical	—	`contsAux` `squashGCF`	—	`Nat.strong_induction_on` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `LT.lt.le` `lt_add_of_pos_right` `zero_lt_two` `le_trans` `squashGCF_nth_of_lt`
`convs_eq_convs'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Pair.a` `Pair.b`	`convs` `Field.toDivisionRing` `convs'`	—	`zeroth_conv_eq_h` `zeroth_conv'_eq_h` `squashGCF_eq_self_of_terminated` `convs_stable_of_terminated` `exists_s_b_of_partDen` `ne_of_lt` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `succ_nth_conv_eq_squashGCF_nth_conv` `Stream'.Seq.ge_stable` `add_pos` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `squashSeq_nth_of_not_terminated` `squashGCF_nth_of_lt` `succ_nth_conv'_eq_squashGCF_nth_conv'`
`squashGCF_eq_self_of_terminated` 📖	mathematical	`TerminatedAt`	`squashGCF`	—	`squashSeq_eq_self_of_terminated`
`squashGCF_nth_of_lt` 📖	mathematical	—	`Stream'.Seq.get?` `Pair` `s` `squashGCF`	—	`squashSeq_nth_of_lt`
`squashSeq_eq_self_of_terminated` 📖	mathematical	`Stream'.Seq.TerminatedAt` `Pair`	`squashSeq`	—	—
`squashSeq_nth_of_lt` 📖	mathematical	—	`Stream'.Seq.get?` `Pair` `squashSeq`	—	`squashSeq_eq_self_of_terminated` `Stream'.Seq.ge_stable` `LT.lt.ne`
`squashSeq_nth_of_not_terminated` 📖	mathematical	`Stream'.Seq.get?` `Pair`	`squashSeq` `Pair.a` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `Pair.b` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid`	—	`Option.map₂_coe_right`
`squashSeq_succ_n_tail_eq_squashSeq_tail_n` 📖	mathematical	—	`Stream'.Seq.tail` `Pair` `squashSeq`	—	`Stream'.Seq.ge_stable` `Stream'.Seq.ext` `Option.map₂_coe_right` `Option.map₂_none_right`
`succ_nth_conv'_eq_squashGCF_nth_conv'` 📖	mathematical	—	`convs'` `squashGCF`	—	`add_zero` `succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq`
`succ_nth_conv_eq_squashGCF_nth_conv` 📖	mathematical	—	`convs` `Field.toDivisionRing` `squashGCF`	—	`squashGCF_eq_self_of_terminated` `convs_stable_of_terminated` `partDen_eq_s_b` `zero_add` `conts_recurrenceAux` `zeroth_contAux_eq_one_zero` `first_contAux_eq_h_one` `mul_one` `MulZeroClass.mul_zero` `add_zero` `div_one` `Stream'.Seq.ge_stable` `squashSeq_nth_of_not_terminated` `conv_eq_conts_a_div_conts_b` `contsAux_recurrence` `contsAux_eq_contsAux_squashGCF_of_le` `le_refl`
`succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq` 📖	mathematical	—	`convs'Aux` `squashSeq`	—	`squashSeq_eq_self_of_terminated` `convs'Aux_stable_step_of_terminated` `Stream'.Seq.ge_stable` `zero_le_one` `Nat.instZeroLEOneClass` `squashSeq_nth_of_not_terminated` `zero_add` `add_zero` `squashSeq_nth_of_lt` `squashSeq_succ_n_tail_eq_squashSeq_tail_n`

---

← Back to Index