Theorem Real.convergent_zero

Modification history

2023-06-16 10:41

Mathlib/NumberTheory/DiophantineApproximation.lean

feat: port NumberTheory.DiophantineApproximation (#5126)

Added Real.convergent_zero View on Github →