Commit 2024-02-12 10:30 6b846c81

View on Github →

fix(positivity): now understands weak 0 < x hypotheses (#10293) This matching used to be done solely by norm_num, but this doesn't work if the type has a zero that's not coupled with the algebraic hierarchy.

Estimated changes