Commit 2023-11-01 01:49 e4ce4443
View on Github →feat: port Rat.cast positivity extension (#8042) See the mathlib3 version here: https://github.com/leanprover-community/mathlib/blob/3365b20c2ffa7c35e47e5209b89ba9abdddf3ffe/src/tactic/positivity.lean#L737-L741