Commit 2023-05-04 09:12 12c37444

View on Github →

feat: port Algebra.ContinuedFractions.Computation.Basic (#3788)

Estimated changes

Modified Mathlib.lean

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

added def GeneralizedContinuedFraction.IntFractPair.coeFn

added theorem GeneralizedContinuedFraction.IntFractPair.coe_to_intFractPair

added def GeneralizedContinuedFraction.IntFractPair.mapFr

added theorem GeneralizedContinuedFraction.IntFractPair.stream_isSeq

added structure GeneralizedContinuedFraction.IntFractPair