maximalIdeal_eq_closedBall — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.Irreducible.maximalIdeal_eq_closedBall [IsDiscreteValuationRing 𝒪[K]] {ϖ : 𝒪[K]} (h : Irreducible ϖ) :
    (𝓂[K] : Set 𝒪[K]) = Metric.closedBall 0 ‖ϖ‖ := by
  simp [h.maximalIdeal_eq_setOf_le_v_coe, Set.ext_iff, ← NNReal.coe_le_coe]

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