maximalIdeal_pow_eq_closedBall_pow

English

For irreducible ϖ and n ∈ ℕ, the n-th power of the maximal ideal equals the closed ball of radius ‖ϖ‖^n.

Русский

Для неприводимого ϖ и натурального n, n-я степень максимального идеала равна замкнутому шару радиуса ‖ϖ‖^n.

LaTeX

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

Lean4

theorem _root_.Irreducible.maximalIdeal_pow_eq_closedBall_pow [IsDiscreteValuationRing 𝒪[K]] {ϖ : 𝒪[K]}
    (h : Irreducible ϖ) (n : ℕ) : ((𝓂[K] ^ n : Ideal 𝒪[K]) : Set 𝒪[K]) = Metric.closedBall 0 (‖ϖ‖ ^ n) := by
  simp [h.maximalIdeal_pow_eq_setOf_le_v_coe_pow, Set.ext_iff, ← NNReal.coe_le_coe]

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