Theorems · Theorem · commutative algebra

Ideal.finprod_count

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

The multiplicity of v in ∏_v v^(val_v(I)) equals val_v(I).

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomain