mathlib

5e58247c - feat(algebra/ordered_pi): ordered_comm_monoid and canonically_ordered_monoid instances (#9194)

feat(algebra/ordered_pi): ordered_comm_monoid and canonically_ordered_monoid instances (#9194) Presumably these instances were missing because they were not actually constructible until we fixed the definition of `ordered_monoid` in #8877!