mathlib3 documentation

algebra.order.monoid.prod

Products of ordered monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]
@[protected, instance]