Commit 2025-07-05 22:44 4ed2ceba
View on Github →feat(Tactic/Positivity): extend EReal support for numeric casts (#26080)
Extend pos_of_isNat and nonneg_of_isNat to cover monoids which are not necessarily semirings, like EReal.
Zulip discussion
feat(Tactic/Positivity): extend EReal support for numeric casts (#26080)
Extend pos_of_isNat and nonneg_of_isNat to cover monoids which are not necessarily semirings, like EReal.
Zulip discussion