Commit 2024-08-27 15:47 a7117bf8

View on Github →

feat: When NNRat.cast is less/greater than 1 (#16137) From LeanAPAP

Estimated changes

added theorem NNRat.cast_le_ofNat
added theorem NNRat.cast_le_one
added theorem NNRat.cast_lt_ofNat
added theorem NNRat.cast_lt_one
added theorem NNRat.ofNat_le_cast
added theorem NNRat.ofNat_lt_cast
added theorem NNRat.one_le_cast
added theorem NNRat.one_lt_cast