Theorem Real.convergent_succ

Modification history

2023-06-16 10:41

Mathlib/NumberTheory/DiophantineApproximation.lean

feat: port NumberTheory.DiophantineApproximation (#5126)

Added Real.convergent_succ View on Github →