Mathlib Changelog
v4
Changelog
About
Github
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