maximalIdeal_pow_eq_setOf_le_v_coe_pow

English

For irreducible ϖ in a DVR O, and for n ∈ ℕ, the nth power of the maximal ideal corresponds to {y ∈ O | v(y) ≤ v(ϖ)^n} (in the subtype setting).

Русский

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

LaTeX

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

Lean4

theorem _root_.Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow [IsDiscreteValuationRing v.integer] {ϖ : v.integer}
    (h : Irreducible ϖ) (n : ℕ) :
    ((IsLocalRing.maximalIdeal v.integer ^ n : Ideal v.integer) : Set v.integer) =
      {y : v.integer | v y ≤ v (ϖ : K) ^ n} :=
  (Valuation.integer.integers v).maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow h _

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