{R : Type u_1} →
  [inst : CommRing R] →
    {f : R → ℝ} →
      {c : ℝ} →
        f 0 = 0 →
          0 ≤ f →
            (∀ (x y : R), f (x * y) ≤ c * f x * f y) →
              (∀ (a b : R), f (a + b) ≤ f a + f b) → (∀ (x : R), f (-x) = f x) → RingSeminorm R