Theorem NNRat.one_lt_cast

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.one_lt_castView on Github →