Theorems · Theorem · commutative algebra

Valuation.Integers.maximalIdeal_eq_setOf_le_v_algebraMap

Deprecated since 2026-07-09Use Valuation.Integers.maximalIdeal_eq_setOfPred_le_v_algebraMap instead.

∀ {K : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : CommRing O] [inst_3 : Algebra O K] {v : Valuation K Γ₀} (hv : v.Integers O)
  [inst_4 : IsDiscreteValuationRing O] {ϖ : O},
  Irreducible ϖ → ↑(IsLocalRing.maximalIdeal O) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ)}

Alias of Valuation.Integers.maximalIdeal_eq_setOfPred_le_v_algebraMap.

Defined in

Mathlib.RingTheory.DiscreteValuationRing.Basic

Cited by

0 results in Mathlib

Foundations

Depth 50 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderedCommGroupWithZeroCommRingAlgebraIsDiscreteValuationRing