Commit 2023-06-17 05:05 cf68008f

View on Github →

feat: port Algebra.ContinuedFractions.Computation.TerminatesIffRat (#5106)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

added theorem GeneralizedContinuedFraction.IntFractPair.coe_of_rat_eq

added theorem GeneralizedContinuedFraction.IntFractPair.coe_stream'_rat_eq

added theorem GeneralizedContinuedFraction.IntFractPair.coe_stream_nth_rat_eq

added theorem GeneralizedContinuedFraction.IntFractPair.exists_nth_stream_eq_none_of_rat

added theorem GeneralizedContinuedFraction.IntFractPair.of_inv_fr_num_lt_num_of_pos

added theorem GeneralizedContinuedFraction.IntFractPair.stream_nth_fr_num_le_fr_num_sub_n_rat

added theorem GeneralizedContinuedFraction.IntFractPair.stream_succ_nth_fr_num_lt_nth_fr_num_rat

added theorem GeneralizedContinuedFraction.coe_of_h_rat_eq

added theorem GeneralizedContinuedFraction.coe_of_rat_eq

added theorem GeneralizedContinuedFraction.coe_of_s_get?_rat_eq

added theorem GeneralizedContinuedFraction.coe_of_s_rat_eq

added theorem GeneralizedContinuedFraction.exists_gcf_pair_rat_eq_nth_conts

added theorem GeneralizedContinuedFraction.exists_rat_eq_nth_convergent

added theorem GeneralizedContinuedFraction.exists_rat_eq_nth_denominator

added theorem GeneralizedContinuedFraction.exists_rat_eq_nth_numerator

added theorem GeneralizedContinuedFraction.exists_rat_eq_of_terminates

added theorem GeneralizedContinuedFraction.of_terminates_iff_of_rat_terminates

added theorem GeneralizedContinuedFraction.terminates_iff_rat

added theorem GeneralizedContinuedFraction.terminates_of_rat