Theorems · Theorem · commutative algebra

Ideal.finprod_not_dvd

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  (I : Ideal R),
  I ≠ 0 →
    ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
        ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I

For every nonzero ideal I of v, v^(val_v(I) + 1) does not divide ∏_v v^(val_v(I)).

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomain