Commit 2026-06-04 15:42 0cbd85e5

View on Github →

chore(Algebra/ContinuedFractions): golf (#38895) This PR simplifies some proofs in Algebra/ContinuedFractions

Estimated changes

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

Modified Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

modified theorem GenContFract.of_h_eq_floor

modified theorem GenContFract.of_h_eq_intFractPair_seq1_fst_b

Modified Mathlib/Algebra/ContinuedFractions/ContinuantsRecurrence.lean

Modified Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean