Commit 2024-12-20 13:13 4649cb13

View on Github →

chore: split material about continued fractions from DiophantineApproximation (#19820)

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/NumberTheory/DiophantineApproximation.lean to Mathlib/NumberTheory/DiophantineApproximation/Basic.lean

deleted theorem Real.convs_eq_convergent

deleted theorem Real.exists_convs_eq_rat

Created Mathlib/NumberTheory/DiophantineApproximation/ContinuedFractions.lean

added theorem Real.convs_eq_convergent

added theorem Real.exists_convs_eq_rat

Modified Mathlib/NumberTheory/Pell.lean