Theorems · Theorem · commutative algebra

Valuation.Integers.maximalIdeal_pow_eq_setOfPred_le_v_algebraMap_pow

∀ {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 ϖ →
    ∀ (n : ℕ), ↑(IsLocalRing.maximalIdeal O ^ n) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ) ^ n}

Defined in: Mathlib.RingTheory.DiscreteValuationRing.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field LinearOrderedCommGroupWithZero CommRing Algebra IsDiscreteValuationRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites23

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
RingHomstatement · cited by 10,189
SetLike.coestatement and proof · cited by 8,199
Fieldstatement and proof · cited by 7,404
Set.ofPredstatement and proof · cited by 6,101
Idealstatement and proof · cited by 4,748
Algebra.algebraMapstatement and proof · cited by 4,706
IsDomainproof · cited by 2,196
Valuationstatement and proof · cited by 823

Cited by2

Results whose statement or proof uses this declaration.

Irreducible.maximalIdeal_pow_eq_setOfPred_le_v_coe_powproof · cited by 3
Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_powproof · cited by 0