Theorems · Theorem · commutative algebra
Ideal.IsPrime.exists_mem_prime_of_ne_bot
∀ {R : Type u_2} [inst : CommSemiring R] [UniqueFactorizationMonoid R] {I : Ideal R},
I.IsPrime → I ≠ ⊥ → ∃ x ∈ I, Prime xEvery non-zero prime ideal in a unique factorization domain contains a prime element.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
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
- Bot.botstatement and proof · cited by 4,720
- Unitsproof · cited by 2,804
- Units.valproof · cited by 1,966
- Ideal.IsPrimestatement and proof · cited by 827
- Multiset.prodproof · cited by 528
- UniqueFactorizationMonoidstatement and proof · cited by 279
- Primestatement · cited by 277
- Units.isUnitproof · cited by 116
- UniqueFactorizationMonoid.factorsproof · cited by 55
- UniqueFactorizationMonoid.factors_prodproof · cited by 18
Cited by3
Results whose statement or proof uses this declaration.
- UniqueFactorizationMonoid.isPrincipal_of_height_eq_oneproof · cited by 2
- UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrimeproof · cited by 1
- IsPrincipalIdealRing.of_isDedekindDomain_of_uniqueFactorizationMonoidproof · cited by 0