Documentation Verification Report

TerminatesIffRat

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

Statistics

Metric	Count
Definitions	0
Theorems `coe_of_rat_eq`, `coe_stream'_rat_eq`, `coe_stream_nth_rat_eq`, `exists_nth_stream_eq_none_of_rat`, `of_inv_fr_num_lt_num_of_pos`, `stream_nth_fr_num_le_fr_num_sub_n_rat`, `stream_succ_nth_fr_num_lt_nth_fr_num_rat`, `coe_of_h_rat_eq`, `coe_of_rat_eq`, `coe_of_s_get?_rat_eq`, `coe_of_s_rat_eq`, `exists_gcf_pair_rat_eq_nth_conts`, `exists_gcf_pair_rat_eq_of_nth_contsAux`, `exists_rat_eq_nth_conv`, `exists_rat_eq_nth_den`, `exists_rat_eq_nth_num`, `exists_rat_eq_of_terminates`, `of_terminates_iff_of_rat_terminates`, `terminates_iff_rat`, `terminates_of_rat`	20
Total	20

GenContFract

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of_h_rat_eq` 📖	mathematical	`DivisionRing.toRatCast` `Field.toDivisionRing`	`h` `of` `Rat.instDivisionRing` `Rat.linearOrder` `Rat.instFloorRing`	—	`of_h_eq_floor` `Rat.cast_intCast` `Rat.floor_cast`
`coe_of_rat_eq` 📖	mathematical	`DivisionRing.toRatCast` `Field.toDivisionRing`	`h` `of` `Rat.instDivisionRing` `Rat.linearOrder` `Rat.instFloorRing` `Stream'.Seq.map` `Pair` `Pair.map` `s`	—	`of_h_eq_floor` `Rat.cast_intCast` `coe_of_s_rat_eq` `Rat.floor_cast` `IntFractPair.stream_isSeq`
`coe_of_s_get?_rat_eq` 📖	mathematical	`DivisionRing.toRatCast` `Field.toDivisionRing`	`Pair` `Pair.map` `Stream'.Seq.get?` `s` `of` `Rat.instDivisionRing` `Rat.linearOrder` `Rat.instFloorRing`	—	`IntFractPair.stream_isSeq` `Stream'.Seq.map_get?` `IntFractPair.coe_stream'_rat_eq` `Rat.cast_one` `Rat.cast_intCast`
`coe_of_s_rat_eq` 📖	mathematical	`DivisionRing.toRatCast` `Field.toDivisionRing`	`Stream'.Seq.map` `Pair` `Pair.map` `s` `of` `Rat.instDivisionRing` `Rat.linearOrder` `Rat.instFloorRing`	—	`Stream'.Seq.ext` `coe_of_s_get?_rat_eq`
`exists_gcf_pair_rat_eq_nth_conts` 📖	mathematical	—	`conts` `Field.toDivisionRing` `of` `Pair.map` `DivisionRing.toRatCast`	—	`nth_cont_eq_succ_nth_contAux` `exists_gcf_pair_rat_eq_of_nth_contsAux`
`exists_gcf_pair_rat_eq_of_nth_contsAux` 📖	mathematical	—	`contsAux` `Field.toDivisionRing` `of` `Pair.map` `DivisionRing.toRatCast`	—	`Nat.strong_induction_on` `Rat.cast_one` `Rat.cast_zero` `of_h_eq_floor` `Rat.cast_intCast` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contsAux_stable_of_terminated` `lt_of_le_of_lt` `of_partNum_eq_one_and_exists_int_partDen_eq` `contsAux_recurrence` `one_mul` `Rat.cast_add` `IsStrictOrderedRing.toCharZero` `Rat.cast_mul`
`exists_rat_eq_nth_conv` 📖	mathematical	—	`convs` `Field.toDivisionRing` `of` `DivisionRing.toRatCast`	—	`exists_rat_eq_nth_num` `exists_rat_eq_nth_den` `Rat.cast_div` `IsStrictOrderedRing.toCharZero`
`exists_rat_eq_nth_den` 📖	mathematical	—	`dens` `Field.toDivisionRing` `of` `DivisionRing.toRatCast`	—	`exists_gcf_pair_rat_eq_nth_conts`
`exists_rat_eq_nth_num` 📖	mathematical	—	`nums` `Field.toDivisionRing` `of` `DivisionRing.toRatCast`	—	`exists_gcf_pair_rat_eq_nth_conts`
`exists_rat_eq_of_terminates` 📖	mathematical	`Terminates` `of` `Field.toDivisionRing`	`DivisionRing.toRatCast`	—	`of_correctness_of_terminates` `exists_rat_eq_nth_conv`
`of_terminates_iff_of_rat_terminates` 📖	mathematical	`DivisionRing.toRatCast` `Field.toDivisionRing`	`Terminates` `of` `Rat.instDivisionRing` `Rat.linearOrder` `Rat.instFloorRing`	—	`coe_of_s_get?_rat_eq`
`terminates_iff_rat` 📖	mathematical	—	`Terminates` `of` `Field.toDivisionRing` `DivisionRing.toRatCast`	—	`exists_rat_eq_of_terminates` `terminates_of_rat` `of_terminates_iff_of_rat_terminates`
`terminates_of_rat` 📖	mathematical	—	`Terminates` `of` `Rat.instDivisionRing` `Rat.linearOrder` `Rat.instFloorRing`	—	`IntFractPair.exists_nth_stream_eq_none_of_rat` `IntFractPair.stream_isSeq` `of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none`

GenContFract.IntFractPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of_rat_eq` 📖	mathematical	`DivisionRing.toRatCast` `Field.toDivisionRing`	`mapFr` `of` `Rat.instDivisionRing` `Rat.linearOrder` `Rat.instFloorRing`	—	`Rat.cast_fract` `Rat.floor_cast`
`coe_stream'_rat_eq` 📖	mathematical	`DivisionRing.toRatCast` `Field.toDivisionRing`	`Stream'.map` `GenContFract.IntFractPair` `mapFr` `stream` `Rat.instDivisionRing` `Rat.linearOrder` `Rat.instFloorRing`	—	`coe_stream_nth_rat_eq`
`coe_stream_nth_rat_eq` 📖	mathematical	`DivisionRing.toRatCast` `Field.toDivisionRing`	`GenContFract.IntFractPair` `mapFr` `stream` `Rat.instDivisionRing` `Rat.linearOrder` `Rat.instFloorRing`	—	`coe_of_rat_eq` `Option.bind_congr'` `Rat.cast_zero` `IsStrictOrderedRing.toCharZero`
`exists_nth_stream_eq_none_of_rat` 📖	mathematical	—	`stream` `Rat.instDivisionRing` `Rat.linearOrder` `Rat.instFloorRing` `GenContFract.IntFractPair`	—	`stream_nth_fr_num_le_fr_num_sub_n_rat` `Int.fract_nonneg` `Rat.instIsStrictOrderedRing` `Nat.cast_add` `Nat.cast_one` `sub_add_eq_sub_sub_swap` `sub_right_comm` `sub_self` `zero_sub` `nth_stream_fr_nonneg_lt_one`
`of_inv_fr_num_lt_num_of_pos` 📖	mathematical	—	`fr` `of` `Rat.instDivisionRing` `Rat.linearOrder` `Rat.instFloorRing`	—	`Rat.fract_inv_num_lt_num_of_pos`
`stream_nth_fr_num_le_fr_num_sub_n_rat` 📖	mathematical	`stream` `Rat.instDivisionRing` `Rat.linearOrder` `Rat.instFloorRing` `GenContFract.IntFractPair`	`fr` `of`	—	`Nat.cast_zero` `sub_zero` `succ_nth_stream_eq_some_iff` `stream_succ_nth_fr_num_lt_nth_fr_num_rat` `le_trans` `sub_add_eq_sub_sub` `le_sub_right_of_add_le` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono`
`stream_succ_nth_fr_num_lt_nth_fr_num_rat` 📖	mathematical	`stream` `Rat.instDivisionRing` `Rat.linearOrder` `Rat.instFloorRing` `GenContFract.IntFractPair`	`fr`	—	`succ_nth_stream_eq_some_iff` `nth_stream_fr_nonneg_lt_one` `Rat.instIsStrictOrderedRing` `lt_of_le_of_ne` `of_inv_fr_num_lt_num_of_pos`

---

← Back to Index