Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-24 08:13 201174d0

View on Github →

feat(algebra/continued_fractions): add basic defs/lemmas for continued fractions (#1433)

feat(algebra/continued_fractions): add basic defs/lemmas for continued fractions
Rename termiantes_at to terminated_at, use long names for cont. fracts.
Fix indentation, remove subfolders, fix docstrings

Estimated changes

Modified docs/references.bib

Created src/algebra/continued_fractions/basic.lean

added theorem continued_fraction.coe_to_generalized_continued_fraction

added theorem continued_fraction.coe_to_simple_continued_fraction

added def continued_fraction

added theorem generalized_continued_fraction.coe_to_generalized_continued_fraction

added def generalized_continued_fraction.continuants

added def generalized_continued_fraction.continuants_aux

added def generalized_continued_fraction.convergents'

added def generalized_continued_fraction.convergents'_aux

added def generalized_continued_fraction.convergents

added def generalized_continued_fraction.denominators

added def generalized_continued_fraction.is_simple_continued_fraction

added def generalized_continued_fraction.next_continuants

added def generalized_continued_fraction.next_denominator

added def generalized_continued_fraction.next_numerator

added def generalized_continued_fraction.numerators

added theorem generalized_continued_fraction.pair.coe_to_generalized_continued_fraction_pair

added def generalized_continued_fraction.partial_denominators

added def generalized_continued_fraction.partial_numerators

added def generalized_continued_fraction.seq.coe_to_seq

added def generalized_continued_fraction.terminated_at

added def generalized_continued_fraction.terminates

added structure generalized_continued_fraction

added theorem simple_continued_fraction.coe_to_generalized_continued_fraction

added def simple_continued_fraction.is_regular_continued_fraction

added def simple_continued_fraction

Created src/algebra/continued_fractions/continuants_recurrence.lean

added theorem generalized_continued_fraction.continuants_aux_recurrence

added theorem generalized_continued_fraction.continuants_recurrence

added theorem generalized_continued_fraction.continuants_recurrence_aux

added theorem generalized_continued_fraction.denominators_recurrence

added theorem generalized_continued_fraction.numerators_recurrence

Created src/algebra/continued_fractions/default.lean

Created src/algebra/continued_fractions/translations.lean

added theorem generalized_continued_fraction.convergent_eq_conts_a_div_conts_b

added theorem generalized_continued_fraction.convergent_eq_num_div_denom

added theorem generalized_continued_fraction.denom_eq_conts_b

added theorem generalized_continued_fraction.first_continuant_aux_eq_h_one

added theorem generalized_continued_fraction.nth_cont_eq_succ_nth_cont_aux

added theorem generalized_continued_fraction.num_eq_conts_a

added theorem generalized_continued_fraction.obtain_conts_a_of_num

added theorem generalized_continued_fraction.obtain_conts_b_of_denom

added theorem generalized_continued_fraction.obtain_s_a_of_part_num

added theorem generalized_continued_fraction.obtain_s_b_of_part_denom

added theorem generalized_continued_fraction.part_denom_eq_s_b

added theorem generalized_continued_fraction.part_denom_none_iff_s_none

added theorem generalized_continued_fraction.part_num_eq_s_a

added theorem generalized_continued_fraction.part_num_none_iff_s_none

added theorem generalized_continued_fraction.terminated_at_iff_part_denom_none

added theorem generalized_continued_fraction.terminated_at_iff_part_num_none

added theorem generalized_continued_fraction.terminated_at_iff_s_none

added theorem generalized_continued_fraction.terminated_at_iff_s_terminated_at

added theorem generalized_continued_fraction.zeroth_continuant_aux_eq_one_zero

added theorem generalized_continued_fraction.zeroth_continuant_eq_h_one

added theorem generalized_continued_fraction.zeroth_convergent'_aux_eq_zero

added theorem generalized_continued_fraction.zeroth_convergent'_eq_h

added theorem generalized_continued_fraction.zeroth_convergent_eq_h

Modified src/data/seq/seq.lean

added def seq.terminated_at

added theorem seq.terminated_stable

added def seq.terminates