spectralNorm_extends_of_finiteDimensional

English

The spectral norm extends the original norm on K: for every k in K, spectralNorm(algebraMap_K_L(k)) = ||k||.

Русский

Спектральная норма расширяет норму на K: для каждого k ∈ K выполняется spectralNorm(algebraMap_K_L(k)) = |k|.

LaTeX

$$$\forall k \in K, \; \operatorname{spectralNorm}_{K,L}(\operatorname{algebraMap}_{K,L}(k)) = \|k\|$$$

Lean4

/-- The spectral norm extends the norm on `K` when `L/K` is finite and normal.
  See also `spectralNorm_extends` for a more general result. -/
theorem spectralNorm_extends_of_finiteDimensional [IsUltrametricDist K] (x : K) :
    spectralNorm K L (algebraMap K L x) = ‖x‖ := by
  rw [spectralNorm_eq_invariantExtension, invariantExtension_extends K L x]

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