∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulPosMono α] {β : Type u_2} [inst_4 : Zero β]
  [inst_5 : Mul β] [inst_6 : Preorder β] (f : β → α),
  f 0 = 0 → (∀ (x y : β), f (x * y) = f x * f y) → (∀ {x y : β}, f x ≤ f y ↔ x ≤ y) → MulPosMono β