Basic

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

Statistics

Metric	Count
Definitions IntFractPair, b, coeFn, fr, inhabited, instRepr, mapFr, of, seq1, stream, of	11
Theorems coe_to_intFractPair, stream_isSeq	2
Total	13

GenContFract

Definitions

Name	Category	Theorems
IntFractPair 📖	CompData	15 math math: IntFractPair.stream_isSeq, IntFractPair.coe_stream_nth_rat_eq, IntFractPair.seq1_fst_eq_of, IntFractPair.coe_stream'_rat_eq, IntFractPair.exists_nth_stream_eq_none_of_rat, IntFractPair.stream_succ_of_int, of_s_head_aux, IntFractPair.succ_nth_stream_eq_none_iff, IntFractPair.get?_seq1_eq_succ_get?_stream, of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, of_h_eq_intFractPair_seq1_fst_b, IntFractPair.stream_zero, of_terminatedAt_iff_intFractPair_seq1_terminatedAt, IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some, IntFractPair.succ_nth_stream_eq_some_iff
of 📖	CompOp	38 math math: of_convergence, coe_of_h_rat_eq, coe_of_s_rat_eq, exists_gcf_pair_rat_eq_nth_conts, exists_rat_eq_nth_num, of_terminates_iff_of_rat_terminates, convs'_succ, compExactValue_correctness_of_stream_eq_some, zero_le_of_den, coe_of_rat_eq, exists_gcf_pair_rat_eq_of_nth_contsAux, of_convergence_epsilon, terminates_iff_rat, convs_succ, of_s_head_aux, coe_of_s_get?_rat_eq, convs'_of_int, of_s_of_int, of_s_head, of_den_mono, Real.exists_convs_eq_rat, of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, of_h_eq_intFractPair_seq1_fst_b, Real.convs_eq_convergent, of_s_tail, get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero, of_terminatedAt_iff_intFractPair_seq1_terminatedAt, zero_le_of_contsAux_b, get?_of_eq_some_of_succ_get?_intFractPair_stream, of_h_eq_floor, terminates_of_rat, of_convs_eq_convs', sub_convs_eq, of_correctness_of_nth_stream_eq_none, exists_rat_eq_nth_conv, of_isSimpContFract, of_s_succ, exists_rat_eq_nth_den

GenContFract.IntFractPair

Definitions

Name	Category	Theorems
b 📖	CompOp	7 math math: GenContFract.of_s_head_aux, one_le_succ_nth_stream_b, GenContFract.of_h_eq_intFractPair_seq1_fst_b, GenContFract.get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero, succ_nth_stream_b_le_nth_stream_fr_inv, exists_succ_get?_stream_of_gcf_of_get?_eq_some, GenContFract.get?_of_eq_some_of_succ_get?_intFractPair_stream
coeFn 📖	CompOp	1 math math: coe_to_intFractPair
fr 📖	CompOp	13 math math: nth_stream_fr_nonneg_lt_one, GenContFract.compExactValue_correctness_of_stream_eq_some, nth_stream_fr_lt_one, stream_succ_nth_fr_num_lt_nth_fr_num_rat, of_inv_fr_num_lt_num_of_pos, succ_nth_stream_eq_none_iff, stream_nth_fr_num_le_fr_num_sub_n_rat, GenContFract.get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero, succ_nth_stream_b_le_nth_stream_fr_inv, GenContFract.sub_convs_eq, succ_nth_stream_eq_some_iff, stream_succ_of_some, nth_stream_fr_nonneg
inhabited 📖	CompOp	—
instRepr 📖	CompOp	—
mapFr 📖	CompOp	3 math math: coe_stream_nth_rat_eq, coe_stream'_rat_eq, coe_of_rat_eq
of 📖	CompOp	8 math math: seq1_fst_eq_of, coe_of_rat_eq, of_inv_fr_num_lt_num_of_pos, stream_nth_fr_num_le_fr_num_sub_n_rat, stream_zero, GenContFract.get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero, succ_nth_stream_eq_some_iff, stream_succ_of_some
seq1 📖	CompOp	4 math math: seq1_fst_eq_of, get?_seq1_eq_succ_get?_stream, GenContFract.of_h_eq_intFractPair_seq1_fst_b, GenContFract.of_terminatedAt_iff_intFractPair_seq1_terminatedAt
stream 📖	CompOp	13 math math: stream_isSeq, coe_stream_nth_rat_eq, coe_stream'_rat_eq, exists_nth_stream_eq_none_of_rat, stream_succ_of_int, GenContFract.of_s_head_aux, succ_nth_stream_eq_none_iff, get?_seq1_eq_succ_get?_stream, GenContFract.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, stream_zero, exists_succ_get?_stream_of_gcf_of_get?_eq_some, succ_nth_stream_eq_some_iff, stream_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_to_intFractPair 📖	mathematical	—	coeFn	—	—
stream_isSeq 📖	mathematical	—	Stream'.IsSeq GenContFract.IntFractPair stream	—	Option.bind_congr'

---

← Back to Index