nnnorm_eq — Mathlib

English

For a number field K, the norm of canonicalEmbedding x equals the maximum of the norms across all embeddings φ: K → ℂ, i.e., the supremum norm principle.

Русский

Для числа поля K норма канонического вложения x равна максимуму норм по всем вложениям φ: K → ℂ.

LaTeX

$$$\\|\\mathrm{canonicalEmbedding}(K)(x)\\|_\\infty = \\sup_{\\phi:K\\to\\mathbb{C}} \\|\\phi(x)\\|_∞$$$

Lean4

theorem nnnorm_eq [NumberField K] (x : K) : ‖canonicalEmbedding K x‖₊ = Finset.univ.sup (fun φ : K →+* ℂ => ‖φ x‖₊) :=
  by simp_rw [Pi.nnnorm_def, apply_at]

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