∀ {S : Type u_5} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Semiring R] {f : R → S},
  (∀ (x : R), 0 ≤ f x) →
    (∀ {x : R}, f x = 0 ↔ x = 0) →
      (∀ (x y : R), f (x + y) ≤ f x + f y) → (∀ (x y : R), f (x * y) = f x * f y) → IsAbsoluteValue f