Theorems · Theorem · commutative algebra

IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg

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

Defined in

Mathlib.RingTheory.DedekindDomain.AdicValuation

Cited by

11 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomain