spectralNorm_extends — Mathlib

English

For every k in K, spectralNorm(K,L)(algebraMap_K_L(k)) equals the norm of k.

Русский

Для каждого k в K спектральная норма удовлетворяет spectralNorm(K,L)(algebraMap_K_L(k)) = ||k||.

LaTeX

$$$\operatorname{spectralNorm}_{K,L}(\mathrm{algebraMap}_{K,L}(k)) = \|k\|$ for all k in K$$

Lean4

/-- The spectral norm extends the norm on `K`. -/
theorem spectralNorm_extends (k : K) : spectralNorm K L (algebraMap K L k) = ‖k‖ :=
  by
  simp_rw [spectralNorm, minpoly.eq_X_sub_C_of_algebraMap_inj _ (algebraMap K L).injective]
  exact spectralValue_X_sub_C k

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