mathlib

44e29dbc - feat(algebra/order/ring/defs): negative versions of order lemmas (#18831)

feat(algebra/order/ring/defs): negative versions of order lemmas (#18831) For each of a handful of lemmas with a `0 <` or `0 ≤` assumption, this adds a variant with a `< 0` or `≤ 0` assumption.