Theorem Mathlib.Meta.Positivity.pos_of_isNat'

Modification history

2025-07-05 22:44
Mathlib/Tactic/Positivity/Core.lean
feat(Tactic/Positivity): extend EReal support for numeric casts (#26080) …
Added Mathlib.Meta.Positivity.pos_of_isNat'View on Github →