Commit 2024-08-20 19:55 5d151347

View on Github →

chore(Data.NNRat.Defs): split file into unbundled and bundled ordered algebra (#15072) We split off the CanonicallyOrderedCommSemiring, CanonicallyLinearOrderedAddCommMonoid, and OrderedSub instances on NNRat to Data.NNRat.Order leaving the remainder independent of bundled ordered algebra classes.

Estimated changes

Modified Mathlib.lean

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

Modified Mathlib/Data/Finset/Density.lean

Modified Mathlib/Data/NNRat/Defs.lean

modified theorem NNRat.mk_natCast

added theorem NNRat.nonpos_iff_eq_zero

modified theorem NNRat.num_pos

Created Mathlib/Data/NNRat/Order.lean

Modified Mathlib/Tactic/Positivity/Basic.lean