Theorems · Theorem · commutative algebra
Ideal.IsPrime.multiset_prod_le
∀ {R : Type u} [inst : CommSemiring R] {s : Multiset (Ideal R)} {P : Ideal R}, P.IsPrime → (s.prod ≤ P ↔ ∃ I ∈ s, I ≤ P)- Defined in
- Mathlib.RingTheory.Ideal.Operations
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Idealstatement and proof · cited by 4,748
- Multisetstatement and proof · cited by 2,627
- Ideal.IsPrimestatement and proof · cited by 827
- Multiset.prodstatement and proof · cited by 528
- Multiset.induction_onproof · cited by 109
- Ideal.one_eq_topproof · cited by 83
- Ideal.IsPrime.ne_topproof · cited by 82
- Multiset.prod_consproof · cited by 68
- Ideal.IsPrime.mul_leproof · cited by 8
Cited by3
Results whose statement or proof uses this declaration.
- PrimeSpectrum.exists_multiset_prod_cons_le_and_prod_not_leproof · cited by 2
- Ideal.IsPrime.pow_le_iffproof · cited by 2
- Ideal.IsPrime.multiset_prod_map_leproof · cited by 2