An instance orphaned from algebra.order.monoid.with_zero.defs #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We put this here to minimise imports: if you can move it back into
algebra.order.monoid.with_zero.defs without increasing imports, please do.
@[protected, instance]
def
with_zero.contravariant_class_mul_lt
{α : Type u}
[has_mul α]
[partial_order α]
[contravariant_class α α has_mul.mul has_lt.lt] :