mem_iff — Mathlib

English

If ϖ is an irreducible element in the valuation ring 𝒪[K], the maximal ideal equals the closed ball of radius ‖ϖ‖.

Русский

Если ϖ неприводим в кольце оценки 𝒪[K], максимальная идеал равен замкнутому шару с радиусом ‖ϖ‖.

LaTeX

$$$$ (\mathfrak{m}[K] : \mathrm{Set} 𝒪[K]) = \mathrm{Metric.closedBall}(0, \|\varpi\|) $$$$

Lean4

/-- An element is in the valuation ring if the norm is bounded by 1. This is a variant of
`Valuation.mem_integer_iff`, phrased using norms instead of the valuation. -/
theorem mem_iff {x : K} : x ∈ 𝒪[K] ↔ ‖x‖ ≤ 1 := by simp [Valuation.mem_integer_iff, ← NNReal.coe_le_coe]

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