Theorem Real.exists_convs_eq_rat

Modification history

2024-12-20 13:13

Mathlib/NumberTheory/DiophantineApproximation/Basic.lean

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

Modified Real.exists_convs_eq_rat View on Github →

2024-07-15 21:27

Mathlib/NumberTheory/DiophantineApproximation.lean

refactor(Mathlib/Algebra/ContinuedFractions/*): generalize determinant formula for continued fraction computation to simple continued fraction (#13555) …

Added Real.exists_convs_eq_rat View on Github →