Theorems · Theorem · commutative algebra

exists_multiset_prod_cons_le_and_prod_not_le

Deprecated since 2026-04-16Use PrimeSpectrum.exists_multiset_prod_cons_le_and_prod_not_le instead.

∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A],
  ¬IsField A →
    ∀ {I M : Ideal A},
      I ≠ ⊥ →
        I ≤ M →
          ∀ [hM : M.IsMaximal],
            ∃ Z,
              (M ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I

Alias of PrimeSpectrum.exists_multiset_prod_cons_le_and_prod_not_le. Specialization of exists_primeSpectrum_prod_le_and_ne_bot_of_domain to Dedekind domains: Let I : Ideal A be a nonzero ideal, where A is a Dedekind domain that is not a field. Then exists_primeSpectrum_prod_le_and_ne_bot_of_domain states we can find a product of prime ideals that is contained within I. This lemma extends that result by making the product minimal: let M be a maximal ideal that contains I, then the product including M is contained within I and the product excluding M is not contained within I.

Defined in

Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainIdeal.IsMaximal