Commit 2021-12-12 01:37 50e318ec
View on Github →feat(algebra/order/ring): pos_iff_pos_of_mul_pos, neg_iff_neg_of_mul_pos (#10634)
Add four lemmas, deducing equivalence of a and b being positive or
negative from such a hypothesis for their product, that don't currently
seem to be present.