Jacobson

📁 Source: Mathlib/RingTheory/Spectrum/Prime/Jacobson.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_isClosed_singleton_of_isJacobsonRing, instJacobsonSpaceOfIsJacobsonRing, isJacobsonRing_iff_jacobsonSpace, isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing	4
Total	4

PrimeSpectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isClosed_singleton_of_isJacobsonRing 📖	mathematical	IsOpen PrimeSpectrum CommRing.toCommSemiring zariskiTopology Set.Nonempty	Set Set.instMembership IsClosed Set.instSingletonSet	—	isClosed_iff_zeroLocus_ideal IsOpen.isClosed_compl Set.notMem_compl_iff Set.Nonempty.ne_empty Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq Set.compl_univ eq_compl_comm zeroLocus_bot zeroLocus_eq_iff Ideal.radical_eq_jacobson le_antisymm le_sInf sInf_le Ideal.IsMaximal.isPrime Ideal.jacobson_mono bot_le
instJacobsonSpaceOfIsJacobsonRing 📖	mathematical	—	JacobsonSpace PrimeSpectrum CommRing.toCommSemiring zariskiTopology	—	jacobsonSpace_iff_locallyClosed compl_eq_comm Set.inter_assoc Mathlib.Tactic.Contrapose.contrapose₄ Ideal.IsMaximal.isPrime isClosed_singleton_iff_isMaximal Ideal.radical_eq_jacobson
isJacobsonRing_iff_jacobsonSpace 📖	mathematical	—	IsJacobsonRing JacobsonSpace PrimeSpectrum CommRing.toCommSemiring zariskiTopology	—	instJacobsonSpaceOfIsJacobsonRing le_antisymm Ideal.IsRadical.radical Ideal.isRadical_jacobson vanishingIdeal_anti_mono JacobsonSpace.closure_inter_closedPoints isClosed_zeroLocus IsClosed.closure_subset_iff sInf_le isClosed_singleton_iff_isMaximal Ideal.le_jacobson
isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing 📖	mathematical	—	List.TFAE IsOpen PrimeSpectrum CommRing.toCommSemiring zariskiTopology Set Set.instSingletonSet IsClopen IsClosed StableUnderGeneralization	—	exists_isClosed_singleton_of_isJacobsonRing Set.mem_singleton IsClopen.isClosed IsOpen.stableUnderGeneralization IsClopen.isOpen Set.ext Set.compl_iUnion IsMin.eq_of_le isMin_iff stableUnderGeneralization_singleton isMax_iff isClosed_singleton_iff_isMaximal IsMax.eq_of_ge Ideal.exists_minimalPrimes_le isPrime bot_le LE.le.trans Eq.ge isOpen_compl_iff Set.Finite.isClosed_biUnion Set.Finite.subset finite_setOf_isMin isClosed_closure List.tfae_of_cycle

---

← Back to Index