Commit 2024-06-09 07:15 4810c69e

View on Github →

feat: order lemmas for NNRat (#13547) This copies the API for order lemmas on Rat

Estimated changes

Modified Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

Modified Mathlib/Data/NNRat/Defs.lean

added theorem NNRat.le_def

added theorem NNRat.lt_def

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

added def Mathlib.Meta.Positivity.evalNNRatCast

added def NNRat.castOrderEmbedding

added theorem NNRat.cast_le

added theorem NNRat.cast_lt

added theorem NNRat.cast_lt_zero

added theorem NNRat.cast_max

added theorem NNRat.cast_min

added theorem NNRat.cast_mono

added theorem NNRat.cast_nonpos

added theorem NNRat.cast_pos

added theorem NNRat.cast_strictMono

added theorem NNRat.not_cast_lt_zero

added theorem NNRat.preimage_cast_Icc

added theorem NNRat.preimage_cast_Ici

added theorem NNRat.preimage_cast_Ico

added theorem NNRat.preimage_cast_Iic

added theorem NNRat.preimage_cast_Iio

added theorem NNRat.preimage_cast_Ioc

added theorem NNRat.preimage_cast_Ioi

added theorem NNRat.preimage_cast_Ioo

added theorem NNRat.preimage_cast_uIcc

added theorem NNRat.preimage_cast_uIoc

Modified test/positivity.lean