English
If L/K is finite and normal, then the spectral norm on L extends to a K-algebra norm on L.
Русский
Если L/К конечномерно и нормально, то спектральная норма на L образует K-алгебраическую норму на L.
LaTeX
$$$\mathrm{spectralNorm}_{K,L}$ is a $K$-algebra norm on $L$.$$
Lean4
/-- The spectral norm is a `K`-algebra norm on `L` when `L/K` is finite and normal.
See also `spectralAlgNorm` for a more general construction. -/
def spectralAlgNorm_of_finiteDimensional_normal [IsUltrametricDist K] : AlgebraNorm K L
where
toFun := spectralNorm K L
map_zero' := by rw [spectralNorm_eq_invariantExtension K L, map_zero]
add_le' := by rw [spectralNorm_eq_invariantExtension]; exact map_add_le_add _
neg' := by rw [spectralNorm_eq_invariantExtension]; exact map_neg_eq_map _
mul_le' := by
simp only [spectralNorm_eq_invariantExtension]
exact map_mul_le_mul (invariantExtension K L)
smul' := by simp [spectralNorm_eq_invariantExtension, AlgebraNormClass.map_smul_eq_mul _]
eq_zero_of_map_eq_zero'
x := by
simp only [spectralNorm_eq_invariantExtension]
exact eq_zero_of_map_eq_zero _
