Commit 2022-12-20 19:46 4ca7b4ef

View on Github →

feat: port Data.Rat.Order (#1116)

depends on: #998

Estimated changes

Modified Mathlib/Data/Rat/Order.lean

added theorem Rat.abs_def

added theorem Rat.divInt_nonneg

added theorem Rat.div_lt_div_iff_mul_lt_mul

added theorem Rat.lt_one_iff_num_lt_denom

added theorem Rat.nonneg_iff_zero_le

added def Rat.numDenCasesOn''.{u}

added theorem Rat.num_nonneg_iff_zero_le

added theorem Rat.num_pos_iff_pos

Modified test/linarith.lean