Theorem Rat.lt_one_iff_num_lt_denom
Modification history
2025-09-19 16:11
Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
chore(Algebra): avoid duplicating proofs by reusing existing theorems or lemmas (#27847)
Modified Rat.lt_one_iff_num_lt_denomView on Github →