Theorems · Definition · commutative algebra

normFromBounded

{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) → f ⁻¹' {0} = {0} → RingNorm R

seminormFromBounded' f as a RingNorm on R, provided that f is nonnegative, multiplicatively bounded and subadditive, that it preserves 0 and negation, and that f has trivial kernel.

Defined in

Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Cited by

0 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing