Theorem exists_div_btwn

Modification history

2025-08-11 10:52
Mathlib/Algebra/Order/Archimedean/Basic.lean
feat: interval in archimedean field contains fraction with large enough denominator (#27424) …
Added exists_div_btwnView on Github →