Noetherian

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

Statistics

Metric	Count
Definitions	0
Theorems exists_not_mem_forall_mem_of_ne, finite_setOf_isMin, instDiscreteTopology, instKrullDimLEOfNatNat, instNoetherianSpace	5
Total	5

IsArtinianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_not_mem_forall_mem_of_ne 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	PrimeSpectrum.isPrime PrimeSpectrum.toPiLocalization_bijective PrimeSpectrum.instDiscreteTopology Pi.single_eq_same IsLocalization.AtPrime.isLocalRing Localization.isLocalization IsLocalization.AtPrime.to_map_mem_maximal_iff Function.Bijective.injective map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_one Pi.single_eq_of_ne AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass

PrimeSpectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_setOf_isMin 📖	mathematical	—	Set.Finite PrimeSpectrum setOf IsMin Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	ext Set.Finite.of_finite_image Set.Finite.subset minimalPrimes.finite_of_isNoetherianRing Set.image_preimage_subset Function.Injective.injOn
instDiscreteTopology 📖	mathematical	—	DiscreteTopology PrimeSpectrum CommRing.toCommSemiring zariskiTopology	—	discreteTopology_iff_finite_and_krullDimLE_zero IsArtinianRing.instFinitePrimeSpectrum instKrullDimLEOfNatNat
instKrullDimLEOfNatNat 📖	mathematical	—	Ring.KrullDimLE CommRing.toCommSemiring	—	Ring.KrullDimLE.mk₀ IsArtinianRing.isMaximal_of_isPrime
instNoetherianSpace 📖	mathematical	—	TopologicalSpace.NoetherianSpace PrimeSpectrum zariskiTopology	—	List.TFAE.out TopologicalSpace.noetherianSpace_TFAE OrderEmbedding.wellFoundedLT instWellFoundedLTOrderDualOfWellFoundedGT wellFoundedGT

---

← Back to Index