ContinuedFractions

Statistics

Metric	Count
Definitions	0
Theorems `convs_eq_convergent`, `exists_convs_eq_rat`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`convs_eq_convergent` 📖	mathematical	—	`GenContFract.convs` `Real` `instDivisionRing` `GenContFract.of` `linearOrder` `instFloorRing` `instRatCast` `convergent`	—	`GenContFract.zeroth_conv_eq_h` `GenContFract.of_h_eq_floor` `Rat.cast_intCast` `GenContFract.convs_succ` `instIsStrictOrderedRing` `convergent_succ` `one_div` `IsStrictOrderedRing.toCharZero`
`exists_convs_eq_rat` 📖	mathematical	`Real` `instLT` `abs` `lattice` `instAddGroup` `instSub` `instRatCast` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `instMonoid`	`GenContFract.convs` `instDivisionRing` `GenContFract.of` `linearOrder` `instFloorRing`	—	`Nat.instAtLeastTwoHAddOfNat` `exists_rat_eq_convergent` `convs_eq_convergent`

---