Theorems · Theorem · commutative algebra

Associates.finite_factors

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R},
  I ≠ 0 →
    ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite,
      ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0

For every nonzero ideal I of v, there are finitely many maximal ideals v such that the multiplicity of v in the factorization of I, denoted val_v(I), is nonzero.

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomain