maximalIdeal_eq_setOf_le_v_coe — Mathlib

English

For irreducible ϖ in a DVR O, the nth power of the maximal ideal equals {y ∈ O | v(y) ≤ v(ϖ)^n} for all n.

Русский

Для неприводимого ϖ в DVR O для всех n выполняется (maximalIdeal)^n = {y | v(y) ≤ v(ϖ)^n}.

LaTeX

$$∀ (n : ℕ), ((IsLocalRing.maximalIdeal O)^n : Set O) = {y : O | v(y) ≤ v(ϖ)^n}$$

Lean4

theorem _root_.Irreducible.maximalIdeal_eq_setOf_le_v_coe [IsDiscreteValuationRing v.integer] {ϖ : v.integer}
    (h : Irreducible ϖ) : (IsLocalRing.maximalIdeal v.integer : Set v.integer) = {y : v.integer | v y ≤ v ϖ} :=
  (Valuation.integer.integers v).maximalIdeal_eq_setOf_le_v_algebraMap h

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