seminormFromConst_seq — Mathlib

English

For a ring seminorm f on R and a fixed element c, the sequence n ↦ f(x c^n)/f(c^n) defines a real-valued sequence associated to x.

Русский

Для кольцевого семинормa f наR и фиксированного элемента c последовательность $n \mapsto f(x c^n)/f(c^n)$ задает вещественную последовательность, зависящую от x.

LaTeX

$$$\text{seminormFromConstSeq}(x) : \mathbb{N} \to \mathbb{R},\; n \mapsto \dfrac{f(x c^n)}{f(c)^n}$$$

Lean4

/-- For a ring seminorm `f` on `R` and `c ∈ R`, the sequence given by `(f (x * c^n))/((f c)^n)`. -/
def seminormFromConst_seq (x : R) : ℕ → ℝ := fun n ↦ f (x * c ^ n) / f c ^ n

Похожие утверждения