Theorems · Theorem · commutative algebra

IsDedekindDomain.HeightOneSpectrum.intValuation_eq_exp_neg_multiplicity

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R},
  r ≠ 0 → v.intValuation r = WithZero.exp (-↑(multiplicity v.asIdeal (Ideal.span {r})))

Defined in

Mathlib.RingTheory.DedekindDomain.AdicValuation

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomain