Theorems · Definition · commutative algebra

algNormFromConst

{K : Type u} →
  [inst : NontriviallyNormedField K] →
    {L : Type v} →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [inst_3 : Algebra.IsAlgebraic K L] →
            [hu : IsUltrametricDist K] → (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1 → {x : L} → x ≠ 0 → AlgebraNorm K L

Given a nonzero x : L, and assuming that (spectralAlgNorm h_alg hna) 1 ≤ 1, this is the real-valued function sending y ∈ L to the limit of (f (y * x^n))/((f x)^n), regarded as an algebra norm.

Defined in

Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldFieldAlgebraAlgebra.IsAlgebraicIsUltrametricDist