Theorems · Theorem · algebraic geometry
IsArtinianRing.exists_not_mem_forall_mem_of_ne
∀ {R : Type u_1} [inst : CommRing R] [IsArtinianRing R] (p : Ideal R) [p.IsPrime],
∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q- Cited by
- 1 results in Mathlib
- Foundations
- Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Idealstatement and proof · cited by 4,748
- Algebra.algebraMapproof · cited by 4,706
- mul_oneproof · cited by 3,885
- map_mulproof · cited by 1,137
- Ideal.IsPrimestatement and proof · cited by 827
- PrimeSpectrumproof · cited by 625
- Pi.singleproof · cited by 518
- Ideal.primeComplproof · cited by 462
- PrimeSpectrum.asIdealproof · cited by 333
- Localization.AtPrimeproof · cited by 299
Cited by1
Results whose statement or proof uses this declaration.
- Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_topproof · cited by 1