mathlib3

50e318ec - feat(algebra/order/ring): pos_iff_pos_of_mul_pos, neg_iff_neg_of_mul_pos (#10634)

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.