Theorems · Theorem · commutative algebra
Ideal.exists_minimalPrimes_le
∀ {R : Type u_1} [inst : CommSemiring R] {I J : Ideal R} [J.IsPrime], I ≤ J → ∃ p ∈ I.minimalPrimes, p ≤ J- Cited by
- 14 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiringIdeal.IsPrime
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement and proof · cited by 53,352
- CommSemiringstatement and proof · cited by 10,911
- Set.ofPredproof · cited by 6,101
- Idealstatement and proof · cited by 4,748
- InfSet.sInfproof · cited by 935
- OrderDualproof · cited by 927
- Ideal.IsPrimestatement and proof · cited by 827
- OrderDual.toDualproof · cited by 481
- OrderDual.ofDualproof · cited by 400
- Maximalproof · cited by 211
- IsChainproof · cited by 158
Cited by14
Results whose statement or proof uses this declaration.
- Ideal.height_monoproof · cited by 10
- Ideal.nonempty_minimalPrimesproof · cited by 7
- Ideal.mem_minimalPrimes_of_height_leproof · cited by 3
- ringKrullDim_quotient_succ_le_of_nonZeroDivisorproof · cited by 3
- Ideal.exists_minimalPrimes_comap_eqproof · cited by 2
- Ideal.sInf_minimalPrimesproof · cited by 2
- PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRingproof · cited by 2
- Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimesproof · cited by 1
- PrimeSpectrum.closure_image_comap_zeroLocusproof · cited by 1
- Ring.krullDimLE_zero_iff_forall_minimalPrimes_isMaximalproof · cited by 1
- UniqueFactorizationMonoid.of_forall_isPrincipal_of_height_eq_oneproof · cited by 1
- Algebra.not_isStronglyTranscendental_of_weaklyQuasiFiniteAtproof · cited by 1