Theorems · Definition · commutative algebra

seminormFromBounded

{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

seminormFromBounded' is a ring seminorm on R.

Defined in: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Cited by: 2 results in Mathlib
Foundations: Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
CommRingstatement and proof · cited by 17,173
RingSeminormstatement · cited by 58
seminormFromBounded'proof · cited by 17
seminormFromBounded_zeroproof · cited by 1
seminormFromBounded_mulproof · cited by 0
seminormFromBounded_negproof · cited by 0
seminormFromBounded_addproof · cited by 0

Cited by3

Results whose statement or proof uses this declaration.

exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensionalproof · cited by 5
normFromBoundedproof · cited by 0
seminormFromBounded_is_norm_iffstatement and proof · cited by 0