spectralNorm_eq — Mathlib

English

The spectral norm on PadicAlgCl p coincides with the usual norm: for all x, spectNorm(x) = ||x||.

Русский

Спектральная норма на PadicAlgCl p совпадает с обычной нормой: для всех x выполняется spectNorm(x) = ||x||.

LaTeX

$$$$\operatorname{spectralNorm}(\mathbb{Q}_p)(x)=\|x\|\quad(x\in \operatorname{PadicAlgCl}(p)).$$$$

Lean4

/-- The norm on `PadicAlgCl p` is the spectral norm induced by the `p`-adic norm on `ℚ_[p]`. -/
@[simp]
theorem spectralNorm_eq (x : PadicAlgCl p) : spectralNorm ℚ_[p] (PadicAlgCl p) x = ‖x‖ :=
  rfl

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