Theorems · Definition · commutative algebra
minimalPrimes
(R : Type u_1) → [inst : CommSemiring R] → Set (Ideal R)
minimalPrimes R is the set of minimal primes of R.
This is defined as Ideal.minimalPrimes ⊥.
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- CommSemiringstatement and proof · cited by 10,911
- Set.ofPredproof · cited by 6,101
- Idealstatement and proof · cited by 4,748
- IsMinimalPrimeproof · cited by 2
Cited by33
Results whose statement or proof uses this declaration.
- Ideal.height_eq_zero_iffstatement and proof · cited by 5
- minimalPrimes_eq_minimalsstatement · cited by 4
- PrimeSpectrum.vanishingIdeal_irreducibleComponentsstatement and proof · cited by 2
- PrimeSpectrum.vanishingIdeal_mem_minimalPrimesstatement and proof · cited by 2
- Ideal.minimalPrimes_eq_comapstatement · cited by 2
- minimalPrimes.finite_of_isNoetherianRingstatement · cited by 2
- IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimesstatement and proof · cited by 2
- PrimeSpectrum.finite_setOfPred_isMinproof · cited by 2
- Ring.KrullDimLE.minimalPrimes_eq_setOfPred_isPrimestatement · cited by 2
- Ideal.mem_minimalPrimes_of_krullDimLE_zerostatement · cited by 2
- Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimesstatement and proof · cited by 2
- PrimeSpectrum.isMin_iffstatement · cited by 1