| Name | Category | Theorems |
|---|
IsSimpContFract 📖 | MathDef | 4 mathmath: ContFract.convs_eq_convs', SimpContFract.determinant, of_isSimpContFract, SimpContFract.determinant_aux
|
Pair 📖 | CompData | 26 mathmath: coe_of_s_rat_eq, exists_gcf_pair_rat_eq_nth_conts, exists_conts_b_of_den, coe_of_rat_eq, exists_gcf_pair_rat_eq_of_nth_contsAux, squashSeq_succ_n_tail_eq_squashSeq_tail_n, of_s_head_aux, coe_of_s_get?_rat_eq, convs'Aux_succ_some, of_s_of_int, of_s_head, squashSeq_nth_of_lt, coe_toGenContFract, exists_conts_a_of_num, exists_s_b_of_partDen, of_s_tail, get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero, partNum_none_iff_s_none, get?_of_eq_some_of_succ_get?_intFractPair_stream, terminatedAt_iff_s_none, exists_s_a_of_partNum, squashSeq_nth_of_not_terminated, terminatedAt_iff_s_terminatedAt, squashGCF_nth_of_lt, of_s_succ, partDen_none_iff_s_none
|
TerminatedAt 📖 | MathDef | 7 mathmath: terminatedAt_iff_partNum_none, of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, terminated_stable, of_terminatedAt_iff_intFractPair_seq1_terminatedAt, terminatedAt_iff_s_none, terminatedAt_iff_s_terminatedAt, terminatedAt_iff_partDen_none
|
Terminates 📖 | MathDef | 3 mathmath: of_terminates_iff_of_rat_terminates, terminates_iff_rat, terminates_of_rat
|
coeFn 📖 | CompOp | 1 mathmath: coe_toGenContFract
|
conts 📖 | CompOp | 12 mathmath: nth_cont_eq_succ_nth_contAux, exists_gcf_pair_rat_eq_nth_conts, first_cont_eq, exists_conts_b_of_den, conts_recurrenceAux, conv_eq_conts_a_div_conts_b, zeroth_cont_eq_h_one, num_eq_conts_a, conts_stable_of_terminated, den_eq_conts_b, exists_conts_a_of_num, conts_recurrence
|
contsAux 📖 | CompOp | 15 mathmath: nth_cont_eq_succ_nth_contAux, compExactValue_correctness_of_stream_eq_some, exists_gcf_pair_rat_eq_of_nth_contsAux, first_contAux_eq_h_one, contsAux_eq_contsAux_squashGCF_of_le, le_of_succ_succ_get?_contsAux_b, zeroth_contAux_eq_one_zero, fib_le_of_contsAux_b, contsAux_stable_of_terminated, second_contAux_eq, zero_le_of_contsAux_b, sub_convs_eq, SimpContFract.determinant_aux, contsAux_stable_step_of_terminated, contsAux_recurrence
|
convs 📖 | CompOp | 21 mathmath: of_convergence, convs_stable_of_terminated, ContFract.convs_eq_convs', abs_sub_convergents_le', of_correctness_of_terminates, succ_nth_conv_eq_squashGCF_nth_conv, conv_eq_conts_a_div_conts_b, of_convergence_epsilon, convs_eq_convs', convs_succ, Real.exists_convs_eq_rat, Real.convs_eq_convergent, of_convs_eq_convs', sub_convs_eq, of_correctness_of_nth_stream_eq_none, exists_rat_eq_nth_conv, conv_eq_num_div_den, of_correctness_atTop_of_terminates, zeroth_conv_eq_h, of_correctness_of_terminatedAt, abs_sub_convs_le
|
convs' 📖 | CompOp | 8 mathmath: ContFract.convs_eq_convs', convs'_succ, zeroth_conv'_eq_h, convs_eq_convs', convs'_of_int, succ_nth_conv'_eq_squashGCF_nth_conv', convs'_stable_of_terminated, of_convs_eq_convs'
|
convs'Aux 📖 | CompOp | 6 mathmath: convs'Aux_stable_step_of_terminated, convs'Aux_succ_some, succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq, zeroth_conv'Aux_eq_zero, convs'Aux_stable_of_terminated, convs'Aux_succ_none
|
dens 📖 | CompOp | 14 mathmath: dens_stable_of_terminated, dens_recurrence, succ_nth_fib_le_of_nth_den, abs_sub_convergents_le', SimpContFract.determinant, zero_le_of_den, den_eq_conts_b, of_den_mono, first_den_eq, zeroth_den_eq_one, le_of_succ_get?_den, conv_eq_num_div_den, abs_sub_convs_le, exists_rat_eq_nth_den
|
h 📖 | CompOp | 14 mathmath: coe_of_h_rat_eq, first_cont_eq, zeroth_num_eq_h, first_num_eq, zeroth_cont_eq_h_one, zeroth_conv'_eq_h, ext_iff, coe_of_rat_eq, first_contAux_eq_h_one, coe_toGenContFract, of_h_eq_intFractPair_seq1_fst_b, second_contAux_eq, of_h_eq_floor, zeroth_conv_eq_h
|
instCoe 📖 | CompOp | — |
instDecidableTerminatedAt 📖 | CompOp | — |
instInhabited 📖 | CompOp | — |
instInhabitedPair 📖 | CompOp | — |
nextConts 📖 | CompOp | — |
nextDen 📖 | CompOp | — |
nextNum 📖 | CompOp | — |
nums 📖 | CompOp | 8 mathmath: nums_stable_of_terminated, exists_rat_eq_nth_num, zeroth_num_eq_h, first_num_eq, SimpContFract.determinant, num_eq_conts_a, nums_recurrence, conv_eq_num_div_den
|
ofInteger 📖 | CompOp | — |
partDens 📖 | CompOp | 3 mathmath: partDen_eq_s_b, terminatedAt_iff_partDen_none, partDen_none_iff_s_none
|
partNums 📖 | CompOp | 3 mathmath: terminatedAt_iff_partNum_none, partNum_eq_s_a, partNum_none_iff_s_none
|
s 📖 | CompOp | 19 mathmath: coe_of_s_rat_eq, ext_iff, coe_of_rat_eq, of_s_head_aux, coe_of_s_get?_rat_eq, of_s_of_int, of_s_head, coe_toGenContFract, exists_s_b_of_partDen, of_s_tail, get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero, partNum_none_iff_s_none, get?_of_eq_some_of_succ_get?_intFractPair_stream, terminatedAt_iff_s_none, exists_s_a_of_partNum, terminatedAt_iff_s_terminatedAt, squashGCF_nth_of_lt, of_s_succ, partDen_none_iff_s_none
|