Commit 2021-10-23 14:30 5f11361a

View on Github →

refactor(algebra/continued_fractions): remove use of open ... as (#9847) Lean 4 doesn't support the use of open ... as ..., so let's get rid of the few uses from mathlib rather than automating it in mathport.

Estimated changes

Modified src/algebra/continued_fractions/basic.lean

modified theorem continued_fraction.coe_to_generalized_continued_fraction

modified theorem continued_fraction.coe_to_simple_continued_fraction

modified def continued_fraction.of_integer

modified theorem generalized_continued_fraction.coe_to_generalized_continued_fraction

modified def generalized_continued_fraction.continuants

modified def generalized_continued_fraction.continuants_aux

modified def generalized_continued_fraction.convergents'

modified def generalized_continued_fraction.convergents'_aux

modified def generalized_continued_fraction.convergents

modified def generalized_continued_fraction.denominators

modified def generalized_continued_fraction.next_continuants

modified def generalized_continued_fraction.numerators

modified def generalized_continued_fraction.of_integer

modified def generalized_continued_fraction.pair.map

modified def generalized_continued_fraction.partial_denominators

modified def generalized_continued_fraction.partial_numerators

modified def generalized_continued_fraction.terminated_at

modified def generalized_continued_fraction.terminates

modified theorem simple_continued_fraction.coe_to_generalized_continued_fraction

modified def simple_continued_fraction.of_integer

Modified src/algebra/continued_fractions/computation/approximation_corollaries.lean

modified theorem generalized_continued_fraction.of_convergents_eq_convergents'

Modified src/algebra/continued_fractions/computation/approximations.lean

modified theorem generalized_continued_fraction.abs_sub_convergents_le

modified theorem generalized_continued_fraction.determinant

modified theorem generalized_continued_fraction.determinant_aux

modified theorem generalized_continued_fraction.fib_le_of_continuants_aux_b

modified theorem generalized_continued_fraction.of_denom_mono

modified theorem generalized_continued_fraction.of_part_num_eq_one

modified theorem generalized_continued_fraction.of_part_num_eq_one_and_exists_int_part_denom_eq

modified theorem generalized_continued_fraction.succ_nth_fib_le_of_nth_denom

modified theorem generalized_continued_fraction.zero_le_of_continuants_aux_b

modified theorem generalized_continued_fraction.zero_le_of_denom

Modified src/algebra/continued_fractions/computation/basic.lean

Modified src/algebra/continued_fractions/computation/correctness_terminating.lean

modified theorem generalized_continued_fraction.of_correctness_at_top_of_terminates

modified theorem generalized_continued_fraction.of_correctness_of_terminated_at

modified theorem generalized_continued_fraction.of_correctness_of_terminates

Modified src/algebra/continued_fractions/computation/terminates_iff_rat.lean

modified theorem generalized_continued_fraction.coe_of_h_rat_eq

modified theorem generalized_continued_fraction.coe_of_rat_eq

modified theorem generalized_continued_fraction.coe_of_s_rat_eq

modified theorem generalized_continued_fraction.exists_rat_eq_nth_convergent

modified theorem generalized_continued_fraction.exists_rat_eq_nth_denominator

modified theorem generalized_continued_fraction.exists_rat_eq_nth_numerator

modified theorem generalized_continued_fraction.exists_rat_eq_of_terminates

modified theorem generalized_continued_fraction.terminates_iff_rat

modified theorem generalized_continued_fraction.terminates_of_rat

Modified src/algebra/continued_fractions/computation/translations.lean

modified theorem generalized_continued_fraction.int_fract_pair.exists_succ_nth_stream_of_gcf_of_nth_eq_some

modified theorem generalized_continued_fraction.of_h_eq_floor

modified theorem generalized_continued_fraction.of_h_eq_int_fract_pair_seq1_fst_b

Modified src/algebra/continued_fractions/continuants_recurrence.lean

modified theorem generalized_continued_fraction.continuants_aux_recurrence

modified theorem generalized_continued_fraction.continuants_recurrence

modified theorem generalized_continued_fraction.continuants_recurrence_aux

modified theorem generalized_continued_fraction.denominators_recurrence

modified theorem generalized_continued_fraction.numerators_recurrence

Modified src/algebra/continued_fractions/convergents_equiv.lean

modified theorem continued_fraction.convergents_eq_convergents'

modified def generalized_continued_fraction.squash_gcf

modified def generalized_continued_fraction.squash_seq

modified theorem generalized_continued_fraction.squash_seq_nth_of_not_terminated

Modified src/algebra/continued_fractions/terminated_stable.lean

modified theorem generalized_continued_fraction.convergents'_aux_stable_of_terminated

modified theorem generalized_continued_fraction.convergents'_aux_stable_step_of_terminated

Modified src/algebra/continued_fractions/translations.lean

modified theorem generalized_continued_fraction.first_continuant_eq

modified theorem generalized_continued_fraction.first_denominator_eq

modified theorem generalized_continued_fraction.first_numerator_eq

modified theorem generalized_continued_fraction.part_denom_eq_s_b

modified theorem generalized_continued_fraction.part_num_eq_s_a

modified theorem generalized_continued_fraction.second_continuant_aux_eq

modified theorem generalized_continued_fraction.zeroth_convergent'_aux_eq_zero