Theorems · Definition · commutative algebra

seminormFromConst_seq

{R : Type u_1} → [inst : CommRing R] → R → RingSeminorm R → R → ℕ → ℝ

For a ring seminorm f on R and c ∈ R, the sequence given by (f (x * c^n))/((f c)^n).

Defined in

Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Cited by

13 results in Mathlib

Foundations

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

Assumes

CommRing