Theorem Rat.num_le_denom_iff

Modification history

2026-02-25 17:28
Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
feat: add a LE version of previous lt_one_iff_num_lt_denom theorem (#35097) …
Added Rat.num_le_denom_iffView on Github →