spectralMulAlgNorm_def — Mathlib

English

Let K be a complete field and L a K-algebra which is algebraic over K. Then for every x in L, the two spectral norms coincide: spectralMulAlgNorm K L x = spectralNorm K L x.

Русский

Пусть K — полное поле, и L — K-алгебра, алгебраическая над K. Для каждого элемента x в L спектральные нормы совпадают: spectralMulAlgNorm K L x = spectralNorm K L x.

LaTeX

$$$\mathrm{spectralMulAlgNorm}(K,L,x) = \mathrm{spectralNorm}(K,L,x)$$$

Lean4

theorem spectralMulAlgNorm_def [CompleteSpace K] (x : L) : spectralMulAlgNorm K L x = spectralNorm K L x :=
  rfl

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