house_eq_sup' — Mathlib

English

For any α in K, the house equals the supremum of the moduli of all its conjugates under the canonical embeddings.

Русский

Для любого α в K дом равен верхней огибающей по модулю всех сопряжённых образов α.

LaTeX

$$$\\operatorname{house}(α) = \\sup_{\\varphi} \\|\\varphi(α)\\|$$$

Lean4

/-- The house is the largest of the modulus of the conjugates of an algebraic number. -/
theorem house_eq_sup' (α : K) : house α = univ.sup' univ_nonempty (fun φ : K →+* ℂ ↦ ‖φ α‖₊) := by
  rw [house, ← coe_nnnorm, nnnorm_eq, ← sup'_eq_sup univ_nonempty]

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