Theorem Real.exists_pi_nat_abs_mul_sub_lt

Modification history

2026-11-10 11:56
Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
feat: simultaneous Dirichlet approximation theorem (#45646) …
Added Real.exists_pi_nat_abs_mul_sub_ltView on Github →