PosMulMono of LinearOrderedCommMonoidWithZero

Stream: mathlib4

[Ira Fesefeldt]

Is there some typeclass instance missing or am missing something?

import Mathlib

example {α : Type u} [LinearOrderedCommMonoidWithZero α] : PosMulMono α := by infer_instance -- fails

I am planning to add a LinearOrderedCommMonoidWithZero instance for unitInterval and it would then be nice to use lemmas from Mathlib.Algebra.Order.GroupWithZero.Unbundled

[Yaël Dillies]

Yes indeed it seems to be missing