Theorem NNRat.cast_strictMono

Modification history

2024-06-09 12:00
Mathlib/Data/Rat/Cast/Order.lean
chore(Data/Rat/Cast/Order): Use `p`, `q` as variable names (#13644) …
Modified NNRat.cast_strictMonoView on Github →
2024-06-09 07:15
Mathlib/Data/Rat/Cast/Order.lean
feat: order lemmas for NNRat (#13547) …
Added NNRat.cast_strictMonoView on Github →