Commit 2024-10-14 23:36 fa858033

View on Github →

feat: add a FloorSemiring instance to NNRat (#13548) Also some missing norm_cast lemmas for inequalities of casts between different types.

Estimated changes

added theorem NNRat.den_one
added theorem NNRat.den_zero
added theorem NNRat.num_one
added theorem NNRat.num_zero
added theorem NNRat.ceil_cast
added theorem NNRat.ceil_coe
added theorem NNRat.coe_ceil
added theorem NNRat.coe_floor
added theorem NNRat.floor_cast
added theorem NNRat.floor_coe
added theorem NNRat.intCeil_cast
added theorem NNRat.intFloor_cast
added theorem NNRat.cast_le_natCast
added theorem NNRat.cast_lt_natCast
added theorem NNRat.natCast_le_cast
added theorem NNRat.natCast_lt_cast
added theorem Rat.cast_le_intCast
added theorem Rat.cast_le_natCast
added theorem Rat.cast_lt_intCast
added theorem Rat.cast_lt_natCast
added theorem Rat.intCast_le_cast
added theorem Rat.intCast_lt_cast
added theorem Rat.natCast_le_cast
added theorem Rat.natCast_lt_cast