English
The reduction shows that algNormFromConst is compatible with the spectral norm construction via the isPowMul_spectralNorm fact.
Русский
Сведение показывает совместимость algNormFromConst с построением спектральной нормы через факт isPowMul_spectralNorm.
LaTeX
$$algNormFromConst_def$$
Lean4
/-- 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. -/
theorem spectralAlgNorm_mul [CompleteSpace K] (x y : L) :
spectralAlgNorm K L (x * y) = spectralAlgNorm K L x * spectralAlgNorm K L y :=
by
by_cases hx : x = 0
· simp [hx, zero_mul, map_zero]
· have hx' : spectralAlgNorm K L x ≠ 0 := ne_of_gt (spectralNorm_zero_lt hx (Algebra.IsAlgebraic.isAlgebraic x))
have hf1 : (spectralAlgNorm K L) 1 ≤ 1 := le_of_eq spectralAlgNorm_one
set f : AlgebraNorm K L := algNormFromConst hf1 hx with hf
have hf_pow : IsPowMul f := seminormFromConst_isPowMul hf1 hx' isPowMul_spectralNorm
rw [← spectralNorm_unique hf_pow, hf]
exact seminormFromConst_const_mul hf1 hx' isPowMul_spectralNorm _
