Commit 2025-05-27 15:51 f6b898cf
View on Github →feat(Tactic/Positivity): support nonnegativity for non-strictly ordered rings (#24868)
Change the positivity extension for multiplication to work on IsOrderedRing when proving nonnegativity instead of needing IsStrictOrderedRing.
Motivated by [#mathlib4 > `positivity` can't apply `mul_nonneg`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60positivity.60.20can't.20apply.20.60mul_nonneg.60/with/516270014).