mathlib3

0449e68c - Generalize some `ordered_comm_monoid` results