Theorems · Theorem · commutative algebra

IsDedekindDomain.HeightOneSpectrum.multiplicity_iSup

∀ {R : Type u_3} [inst : CommRing R] [IsDedekindDomain R] (p : IsDedekindDomain.HeightOneSpectrum R) {ι : Type u_4}
  [Finite ι] [Nonempty ι] {I : ι → Ideal R},
  (∀ (i : ι), I i ≠ ⊥) → multiplicity p.asIdeal (⨆ i, I i) = ⨅ i, multiplicity p.asIdeal (I i)

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainFiniteNonempty