Commit 2023-05-04 19:07 d1ae7b1b

View on Github →

feat: port Algebra.ContinuedFractions.ConvergentsEquiv (#3795)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean

added theorem GeneralizedContinuedFraction.continuantsAux_eq_continuantsAux_squashGCF_of_le

added theorem GeneralizedContinuedFraction.convergents_eq_convergents'

added def GeneralizedContinuedFraction.squashGCF

added theorem GeneralizedContinuedFraction.squashGCF_eq_self_of_terminated

added theorem GeneralizedContinuedFraction.squashGCF_nth_of_lt

added def GeneralizedContinuedFraction.squashSeq

added theorem GeneralizedContinuedFraction.squashSeq_eq_self_of_terminated

added theorem GeneralizedContinuedFraction.squashSeq_nth_of_lt

added theorem GeneralizedContinuedFraction.squashSeq_nth_of_not_terminated

added theorem GeneralizedContinuedFraction.squashSeq_succ_n_tail_eq_squashSeq_tail_n

added theorem GeneralizedContinuedFraction.succ_nth_convergent'_eq_squashGCF_nth_convergent'

added theorem GeneralizedContinuedFraction.succ_nth_convergent_eq_squashGCF_nth_convergent

added theorem GeneralizedContinuedFraction.succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq