Theorems · Definition · commutative algebra
Ideal.IsMinimalPrime
{R : Type u_1} → [inst : CommSemiring R] → Ideal R → Ideal R → PropIsMinimalPrime I p says that p is a minimal prime over I.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Ideal.IsPrimeproof · cited by 827
- Minimalproof · cited by 150
Cited by7
Results whose statement or proof uses this declaration.
- Ideal.minimalPrimesproof · cited by 74
- Ideal.IsMinimalPrime.isPrimestatement and proof · cited by 26
- Ideal.IsMinimalPrime.lestatement and proof · cited by 23
- Ideal.height_le_spanRank_toENat_of_mem_minimalPrimesproof · cited by 5
- IsMinimalPrimeproof · cited by 2
- Ideal.iUnion_minimalPrimesproof · cited by 1
- Ideal.radical_minimalPrimesproof · cited by 1