An instance orphaned from Algebra.Order.Monoid.WithZero.Defs

We put this here to minimise imports: if you can move it back into Algebra.Order.Monoid.WithZero.Defs without increasing imports, please do.

instance WithZero.contravariantClass_mul_lt {α : Type u} [Mul α] [PartialOrder α] [ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] : ContravariantClass (WithZero α) (WithZero α) (fun (x x_1 : WithZero α) => x * x_1) fun (x x_1 : WithZero α) => x < x_1

Equations

• One or more equations did not get rendered due to their size.