Def Mathlib.Meta.Positivity.evalNNRatCast

Modification history

2025-11-19 06:07
Mathlib/Data/Rat/Cast/Order.lean
chore: move Mathlib to the module system (#31786) …
Deleted Mathlib.Meta.Positivity.evalNNRatCastView on Github →
2024-06-09 07:15
Mathlib/Data/Rat/Cast/Order.lean
feat: order lemmas for NNRat (#13547) …
Added Mathlib.Meta.Positivity.evalNNRatCastView on Github →