Theorem Real.convergent_of_int

Modification history

2023-06-16 10:41

Mathlib/NumberTheory/DiophantineApproximation.lean

feat: port NumberTheory.DiophantineApproximation (#5126)

Added Real.convergent_of_int View on Github →