Basic

📁 Source: Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean

Statistics

Metric	Count
Definitions minimalPrimes, minimalPrimes	2
Theorems eq_bot_of_minimalPrimes_eq_empty, exists_minimalPrimes_le, map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes, mem_minimalPrimes_sup, minimalPrimes_eq_empty_iff, minimalPrimes_eq_subsingleton, minimalPrimes_eq_subsingleton_self, minimalPrimes_isPrime, minimalPrimes_top, nonempty_minimalPrimes, radical_minimalPrimes, sInf_minimalPrimes, minimalPrimes_eq_singleton_bot, minimalPrimes_eq_minimals	14
Total	16

Ideal

Definitions

Name	Category	Theorems
minimalPrimes 📖	CompOp	24 math math: IsLocalization.minimalPrimes_map, height_le_iff_exists_minimalPrimes, exists_finset_card_eq_height_of_isNoetherianRing, minimalPrimes_top, mem_minimalPrimes_of_height_eq, minimalPrimes_eq_subsingleton, nonempty_minimalPrimes, finite_minimalPrimes_of_isNoetherianRing, IsMinimalPrimaryDecomposition.minimalPrimes_subset_image_radical, IsLocalization.minimalPrimes_comap, Ring.KrullDimLE.mem_minimalPrimes_iff_le_of_isPrime, minimalPrimes_eq_comap, exists_minimalPrimes_le, minimalPrimes_map_of_surjective, Ring.KrullDimLE.mem_minimalPrimes_iff, Module.associatedPrimes.minimalPrimes_annihilator_subset_associatedPrimes, minimalPrimes_eq_subsingleton_self, comap_minimalPrimes_eq_of_surjective, mem_minimalPrimes_of_primeHeight_eq_height, radical_minimalPrimes, minimalPrimes_comap_subset, minimalPrimes_eq_empty_iff, sInf_minimalPrimes, iUnion_minimalPrimes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_bot_of_minimalPrimes_eq_empty 📖	mathematical	minimalPrimes Set Ideal CommSemiring.toSemiring Set.instEmptyCollection	Top.top Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	nonempty_minimalPrimes Set.notMem_empty
exists_minimalPrimes_le 📖	mathematical	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Set Set.instMembership minimalPrimes	—	zorn_le_nonempty₀ sInf_isPrime_of_isChain IsChain.symm OrderDual.ofDual_toDual le_sInf_iff OrderDual.le_toDual sInf_le Maximal.prop Maximal.le_of_ge
map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes 📖	mathematical	Ideal CommSemiring.toSemiring Set Set.instMembership minimalPrimes CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule HasQuotient.Quotient Ring.toSemiring CommRing.toRing instHasQuotient map RingHom RingHom.instFunLike algebraMap Quotient.semiring Quotient.commSemiring Quotient.ring instIsTwoSided_1	SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Algebra.id	—	instIsTwoSided_1 sup_le_iff RingHom.instRingHomClass map_le_iff_le_comap under_def over_def IsPrime.under le_trans le_comap_map comap_mono LiesOver.over isPrime_map_quotientMk_of_isPrime map_mono comap_map_quotientMk sup_of_le_right
mem_minimalPrimes_sup 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule HasQuotient.Quotient Ring.toSemiring CommRing.toRing instHasQuotient Quotient.semiring Set Quotient.commSemiring Set.instMembership minimalPrimes map RingHom Quotient.ring instIsTwoSided_1 RingHom.instFunLike	SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Algebra.id	—	instIsTwoSided_1 sup_le_iff RingHom.instRingHomClass comap_map_quotientMk sup_of_le_right comap_mono isPrime_map_quotientMk_of_isPrime map_mono
minimalPrimes_eq_empty_iff 📖	mathematical	—	minimalPrimes Set Ideal CommSemiring.toSemiring Set.instEmptyCollection Top.top Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	exists_le_maximal exists_minimalPrimes_le IsMaximal.isPrime' Set.notMem_empty minimalPrimes_top
minimalPrimes_eq_subsingleton 📖	mathematical	IsPrimary	minimalPrimes Ideal CommSemiring.toSemiring Set Set.instSingletonSet radical	—	Set.ext IsPrime.radical_le_iff LE.le.antisymm isPrime_radical le_radical
minimalPrimes_eq_subsingleton_self 📖	mathematical	—	minimalPrimes Ideal CommSemiring.toSemiring Set Set.instSingletonSet	—	Set.ext LE.le.antisymm Eq.le
minimalPrimes_isPrime 📖	mathematical	Ideal CommSemiring.toSemiring Set Set.instMembership minimalPrimes	IsPrime	—	—
minimalPrimes_top 📖	mathematical	—	minimalPrimes Top.top Ideal CommSemiring.toSemiring Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Set Set.instEmptyCollection	—	Set.ext IsPrime.ne_top top_le_iff
nonempty_minimalPrimes 📖	mathematical	—	Set.Elem Ideal CommSemiring.toSemiring minimalPrimes	—	exists_le_maximal exists_minimalPrimes_le IsMaximal.isPrime'
radical_minimalPrimes 📖	mathematical	—	minimalPrimes radical	—	minimalPrimes.eq_1 Set.ext IsPrime.radical_le_iff
sInf_minimalPrimes 📖	mathematical	—	InfSet.sInf Ideal CommSemiring.toSemiring Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule minimalPrimes radical	—	radical_eq_sInf le_antisymm mem_sInf exists_minimalPrimes_le sInf_le_sInf

IsDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
minimalPrimes_eq_singleton_bot 📖	mathematical	—	minimalPrimes Ideal CommSemiring.toSemiring Set Set.instSingletonSet Bot.bot Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.minimalPrimes_eq_subsingleton_self Ideal.isPrime_bot toNontrivial to_noZeroDivisors

(root)

Definitions

Name	Category	Theorems
minimalPrimes 📖	CompOp	16 math math: minimalPrimes_eq_minimals, PrimeSpectrum.vanishingIdeal_irreducibleComponents, Ring.KrullDimLE.minimalPrimes_eq_setOf_isPrime, PrimeSpectrum.zeroLocus_minimalPrimes, PrimeSpectrum.isMin_iff, Ring.krullDimLE_one_iff, minimalPrimes.finite_of_isNoetherianRing, IsDomain.minimalPrimes_eq_singleton_bot, PrimeSpectrum.zeroLocus_ideal_mem_irreducibleComponents, Ideal.minimalPrimes_eq_comap, Ideal.primeHeight_eq_zero_iff, Ring.KrullDimLE.minimalPrimes_eq_setOf_isMaximal, PrimeSpectrum.stableUnderGeneralization_singleton, Ideal.mem_minimalPrimes_iff_isPrime, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes, Ideal.mem_minimalPrimes_of_krullDimLE_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
minimalPrimes_eq_minimals 📖	mathematical	—	minimalPrimes setOf Ideal CommSemiring.toSemiring Minimal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.IsPrime	—	—

---

← Back to Index