Powers of the maximal ideal of a discrete valuation ring

The maximal ideal of a discrete valuation ring is generated by a uniformizer, so membership in its n-th power is the inequality n ≤ v x for the additive valuation IsDiscreteValuationRing.addVal, and the principal ideal generated by a nonzero x is 𝔪 ^ (v x). Mathlib inlines these rewrites where it needs them; this file states them once.

Main results

• TauCeti.IsDiscreteValuationRing.mem_maximalIdeal_pow_iff_le_addVal: x ∈ 𝔪 ^ n is n ≤ addVal x.
• TauCeti.IsDiscreteValuationRing.addVal_eq_multiplicity_span_singleton: for x ≠ 0, addVal x is the multiplicity of 𝔪 in the ideal (x).

theorem TauCeti.IsDiscreteValuationRing.mem_maximalIdeal_pow_iff_le_addVal {S : Type u_1} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] {n : ℕ} {x : S} : x ∈ IsLocalRing.maximalIdeal S ^ n ↔ ↑n ≤ (IsDiscreteValuationRing.addVal S) x

Membership in a power of the maximal ideal of a discrete valuation ring, read on the additive valuation.

theorem TauCeti.IsDiscreteValuationRing.addVal_eq_multiplicity_span_singleton {S : Type u_1} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] {x : S} (hx : x ≠ 0) : (IsDiscreteValuationRing.addVal S) x = ↑(multiplicity (IsLocalRing.maximalIdeal S) (Ideal.span {x}))

The additive valuation of a nonzero element of a discrete valuation ring is the multiplicity of the maximal ideal in the principal ideal it generates.