ApproximationCorollaries

📁 Source: Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean

Statistics

Metric	Count
Definitions	0
Theorems convs_succ, of_convergence, of_convergence_epsilon, of_convs_eq_convs'	4
Total	4

GenContFract

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convs_succ 📖	mathematical	—	convs Field.toDivisionRing of Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Int.floor DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Int.fract	—	of_convs_eq_convs' convs'_succ
of_convergence 📖	mathematical	—	Filter.Tendsto convs Field.toDivisionRing of Filter.atTop Nat.instPreorder nhds	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing abs_sub_comm instIsDirectedOrder Nat.instIsStrictOrderedRing instArchimedeanNat of_convergence_epsilon
of_convergence_epsilon 📖	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	abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SubNegMonoid.toSub AddGroup.toSubNegMonoid convs of	—	exists_nat_gt of_correctness_of_terminatedAt sub_eq_zero Nat.cast_zero Nat.abs_cast IsStrictOrderedRing.toIsOrderedRing abs_sub_convs_le succ_nth_fib_le_of_nth_den terminated_stable LE.le.trans_lt' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero Nat.fib_pos mul_pos IsStrictOrderedRing.toPosMulStrictMono div_lt_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono le_max_left Nat.le_fib_self le_trans le_max_right Nat.fib_le_fib_succ Nat.mono_cast Nat.cast_nonneg' mul_le_mul IsOrderedRing.toMulPosMono le_of_lt div_lt_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono lt_of_le_of_lt
of_convs_eq_convs' 📖	mathematical	—	convs Field.toDivisionRing of convs'	—	ContFract.convs_eq_convs'

---

← Back to Index