Commit 2023-06-16 05:40 eae91c7a

View on Github →

feat: port Algebra.ContinuedFractions.Computation.ApproximationCorollaries (#5103)

Estimated changes

Modified Mathlib.lean

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

added def ContinuedFraction.of

added theorem GeneralizedContinuedFraction.convergents_succ

added theorem GeneralizedContinuedFraction.of_convergence

added theorem GeneralizedContinuedFraction.of_convergence_epsilon

added theorem GeneralizedContinuedFraction.of_convergents_eq_convergents'

added theorem GeneralizedContinuedFraction.of_isSimpleContinuedFraction

added theorem SimpleContinuedFraction.of_isContinuedFraction