Theorems · Theorem · commutative algebra

seminormFromConst_apply_of_isMul

∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 → f c ≠ 0 → IsPowMul ⇑f → ∀ {x : R}, (∀ (y : R), f (x * y) = f x * f y) → seminormFromConst' c f x = f x

If x : R is multiplicative for f, then seminormFromConst' c f x = f x.

Defined in

Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing