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