Commit 2023-05-04 08:21 96a2d911

View on Github →

feat: port Algebra.ContinuedFractions.ContinuantsRecurrence (#3791)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/ContinuedFractions/ContinuantsRecurrence.lean

added theorem GeneralizedContinuedFraction.continuantsAux_recurrence

added theorem GeneralizedContinuedFraction.continuants_recurrence

added theorem GeneralizedContinuedFraction.continuants_recurrenceAux

added theorem GeneralizedContinuedFraction.denominators_recurrence

added theorem GeneralizedContinuedFraction.numerators_recurrence