Theorems · Theorem · commutative algebra

spectralAlgNorm_mul

∀ {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] [CompleteSpace K] (x y : L),
  (spectralAlgNorm K L) (x * y) = (spectralAlgNorm K L) x * (spectralAlgNorm K L) y

If K is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and L/K is an algebraic extension, then the spectral norm on L is multiplicative.

Defined in

Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldFieldAlgebraAlgebra.IsAlgebraicIsUltrametricDistCompleteSpace