Theorems · Theorem · commutative algebra

IsDedekindDomain.HeightOneSpectrum.inf_pow_eq_prod

∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_4} [IsDedekindDomain R] (s : Finset ι) (e : ι → ℕ)
  (f : ι → IsDedekindDomain.HeightOneSpectrum R),
  (∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j) → (s.inf fun i => (f i).asIdeal ^ e i) = ∏ i ∈ s, (f i).asIdeal ^ e i

The intersection of distinct prime powers in a Dedekind domain is the product of these prime powers. See IsDedekindDomain.inf_pow_eq_prod_of_prime for the version in terms of Ideal R.

Defined in

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomain