English
Let L/K be a finite, normal extension with K equipped with an ultrametric distance. Then the spectral norm on L is power-multiplicative, i.e., for every x in L and every natural n, spectralNorm(K,L)(x^n) = spectralNorm(K,L)(x)^n.
Русский
Пусть L/K — конечное нормальное расширение, а на K задано ультраметрическое расстояние. Тогда спектральная норма на L является степенно-множимой: для любого x ∈ L и любого натурального n выполняется spectralNorm(K,L)(x^n) = spectralNorm(K,L)(x)^n.
LaTeX
$$$\forall x \in L, \forall n \in \mathbb{N}, \; \operatorname{spectralNorm}_{K,L}(x^n) = \operatorname{spectralNorm}_{K,L}(x)^n$$$
Lean4
/-- If `L/K` is finite and normal, then `spectralNorm K L` is power-multiplicative.
See also the more general result `isPowMul_spectralNorm`. -/
theorem isPowMul_spectralNorm_of_finiteDimensional_normal [IsUltrametricDist K] : IsPowMul (spectralNorm K L) :=
by
rw [spectralNorm_eq_invariantExtension K L]
exact isPowMul_invariantExtension K L
