Commit 2023-05-04 05:47 a1e6ff67

View on Github →

feat: port Algebra.ContinuedFractions.Translations (#3783)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/ContinuedFractions/Translations.lean

added theorem GeneralizedContinuedFraction.convergent_eq_conts_a_div_conts_b

added theorem GeneralizedContinuedFraction.convergent_eq_num_div_denom

added theorem GeneralizedContinuedFraction.convergents'Aux_succ_none

added theorem GeneralizedContinuedFraction.convergents'Aux_succ_some

added theorem GeneralizedContinuedFraction.denom_eq_conts_b

added theorem GeneralizedContinuedFraction.exists_conts_a_of_num

added theorem GeneralizedContinuedFraction.exists_conts_b_of_denom

added theorem GeneralizedContinuedFraction.exists_s_a_of_part_num

added theorem GeneralizedContinuedFraction.exists_s_b_of_part_denom

added theorem GeneralizedContinuedFraction.first_continuant_aux_eq_h_one

added theorem GeneralizedContinuedFraction.first_continuant_eq

added theorem GeneralizedContinuedFraction.first_denominator_eq

added theorem GeneralizedContinuedFraction.first_numerator_eq

added theorem GeneralizedContinuedFraction.nth_cont_eq_succ_nth_cont_aux

added theorem GeneralizedContinuedFraction.num_eq_conts_a

added theorem GeneralizedContinuedFraction.part_denom_eq_s_b

added theorem GeneralizedContinuedFraction.part_denom_none_iff_s_none

added theorem GeneralizedContinuedFraction.part_num_eq_s_a

added theorem GeneralizedContinuedFraction.part_num_none_iff_s_none

added theorem GeneralizedContinuedFraction.second_continuant_aux_eq

added theorem GeneralizedContinuedFraction.terminatedAt_iff_part_denom_none

added theorem GeneralizedContinuedFraction.terminatedAt_iff_part_num_none

added theorem GeneralizedContinuedFraction.terminatedAt_iff_s_none

added theorem GeneralizedContinuedFraction.terminatedAt_iff_s_terminatedAt

added theorem GeneralizedContinuedFraction.zeroth_continuant_aux_eq_one_zero

added theorem GeneralizedContinuedFraction.zeroth_continuant_eq_h_one

added theorem GeneralizedContinuedFraction.zeroth_convergent'_aux_eq_zero

added theorem GeneralizedContinuedFraction.zeroth_convergent'_eq_h

added theorem GeneralizedContinuedFraction.zeroth_convergent_eq_h

added theorem GeneralizedContinuedFraction.zeroth_denominator_eq_one

added theorem GeneralizedContinuedFraction.zeroth_numerator_eq_h