∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R),
  μ 1 ≤ 1 →
    ∀ {x : R},
      (∀ (y : R), μ (x * y) = μ x * μ y) → ∀ (y : R), smoothingFun μ (x * y) = smoothingFun μ x * smoothingFun μ y