Theorems · Theorem · commutative algebra
Ideal.mem_sInf
∀ {R : Type u} [inst : Semiring R] {s : Set (Ideal R)} {x : R}, x ∈ sInf s ↔ ∀ ⦃I : Ideal R⦄, I ∈ s → x ∈ I- Defined in
- Mathlib.RingTheory.Ideal.Lattice
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Semiringstatement and proof · cited by 13,802
- SetLike.coeproof · cited by 8,199
- Submoduleproof · cited by 7,192
- Idealstatement and proof · cited by 4,748
- Set.rangeproof · cited by 4,705
- Set.iInterproof · cited by 1,084
- InfSet.sInfstatement and proof · cited by 935
- iInf_posproof · cited by 31
Cited by15
Results whose statement or proof uses this declaration.
- Ideal.le_jacobsonproof · cited by 9
- Ideal.jacobson_monoproof · cited by 6
- isJacobsonRing_iff_prime_eqproof · cited by 5
- LocalizedModule.subsingleton_iff_support_subsetproof · cited by 5
- IsLocalization.isMaximal_iff_isMaximal_disjointproof · cited by 3
- Ideal.eq_jacobson_iff_sInf_maximalproof · cited by 2
- Ideal.sInf_minimalPrimesproof · cited by 2
- PrimeSpectrum.mem_image_comap_zeroLocus_sdiffproof · cited by 2
- Ideal.mem_jacobson_iffproof · cited by 2
- isJacobsonRing_localizationproof · cited by 1
- MvPolynomial.radical_le_vanishingIdeal_zeroLocusproof · cited by 1
- Ideal.sInf_isPrime_of_isChainproof · cited by 1