Commit 2024-08-17 13:18 67d7502b

View on Github →

chore(Algebra.Order.Ring.Rat): split into unbundled and bundled ordered algebra results (#15071) We split off all but the LinearOrderedCommRing and the inferred OrderedAddCommMonoid instances on Rat into Algebra.Order.Ring.Unbundled.Rat as these results do not require bundled ordered algebra classes.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Ring/Rat.lean

deleted theorem NNRat.cast_ofScientific

deleted theorem Rat.abs_def

deleted theorem Rat.divInt_nonneg

deleted theorem Rat.divInt_nonneg_iff_of_pos_right

deleted theorem Rat.div_lt_div_iff_mul_lt_mul

deleted theorem Rat.lt_one_iff_num_lt_denom

deleted theorem Rat.mkRat_nonneg

deleted theorem Rat.num_neg

deleted theorem Rat.num_nonpos

deleted theorem Rat.num_pos

deleted theorem Rat.ofScientific_nonneg

Created Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

added theorem NNRat.cast_ofScientific

added theorem Rat.abs_def

added theorem Rat.divInt_nonneg

added theorem Rat.divInt_nonneg_iff_of_pos_right

added theorem Rat.div_lt_div_iff_mul_lt_mul

added theorem Rat.lt_one_iff_num_lt_denom

added theorem Rat.mkRat_nonneg

added theorem Rat.num_neg

added theorem Rat.num_nonpos

added theorem Rat.num_pos

added theorem Rat.ofScientific_nonneg

Modified Mathlib/Data/FP/Basic.lean

Modified Mathlib/Data/Int/Star.lean

Modified Mathlib/Data/NNRat/Defs.lean

modified def NNRat.divNat

Modified Mathlib/Data/Rat/Cast/Lemmas.lean