Commit 2023-05-03 13:39 1a306e63

View on Github →

feat: port Algebra.ContinuedFractions.Basic (#3379)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/ContinuedFractions/Basic.lean

added def ContinuedFraction.ofInteger

added def ContinuedFraction

added def GeneralizedContinuedFraction.IsSimpleContinuedFraction

added def GeneralizedContinuedFraction.Pair.coeFn

added theorem GeneralizedContinuedFraction.Pair.coe_toPair

added def GeneralizedContinuedFraction.Pair.map

added structure GeneralizedContinuedFraction.Pair

added def GeneralizedContinuedFraction.TerminatedAt

added def GeneralizedContinuedFraction.Terminates

added def GeneralizedContinuedFraction.coeFn

added theorem GeneralizedContinuedFraction.coe_toGeneralizedContinuedFraction

added def GeneralizedContinuedFraction.continuants

added def GeneralizedContinuedFraction.continuantsAux

added def GeneralizedContinuedFraction.convergents'

added def GeneralizedContinuedFraction.convergents'Aux

added def GeneralizedContinuedFraction.convergents

added def GeneralizedContinuedFraction.denominators

added def GeneralizedContinuedFraction.nextContinuants

added def GeneralizedContinuedFraction.nextDenominator

added def GeneralizedContinuedFraction.nextNumerator

added def GeneralizedContinuedFraction.numerators

added def GeneralizedContinuedFraction.ofInteger

added def GeneralizedContinuedFraction.partialDenominators

added def GeneralizedContinuedFraction.partialNumerators

added structure GeneralizedContinuedFraction

added def SimpleContinuedFraction.IsContinuedFraction

added def SimpleContinuedFraction.ofInteger

added def SimpleContinuedFraction