Theorem NNRat.cast_le_one

Modification history

2024-08-27 15:47
Mathlib/Data/Rat/Cast/Order.lean
feat: When `NNRat.cast` is less/greater than `1` (#16137) …
Added NNRat.cast_le_oneView on Github →