Basic

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

Statistics

Metric	Count
Definitions IsAssociatedPrime, IsAssociatedPrime, associatedPrimes, associatedPrimes	4
Theorems mem_iff, mem_iff, annihilator_le, eq_radical, isPrime, map_of_injective, eq, isAssociatedPrime_iff, mem_iff, eq_radical_colon, toIsPrime, instIsPrimeValIdealMemSetAssociatedPrimes, isAssociatedPrime_def, isAssociatedPrime_iff, eq_empty_of_subsingleton, eq_singleton_of_isPrimary, nonempty, prod, subset_of_injective, subset_union_of_exact, biUnion_associatedPrimes_eq_compl_nonZeroDivisors, biUnion_associatedPrimes_eq_zero_divisors, exists_le_isAssociatedPrime_of_isNoetherianRing, instIsPrimeValIdealMemSetAssociatedPrimes, isAssociatedPrime_iff, isAssociatedPrime_iff_exists_injective_linearMap, not_isAssociatedPrime_of_subsingleton	27
Total	31

AssociatePrimes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_iff 📖	mathematical	—	Ideal CommSemiring.toSemiring Set Set.instMembership associatedPrimes IsAssociatedPrime	—	AssociatedPrimes.mem_iff

AssociatedPrimes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_iff 📖	mathematical	—	Ideal CommSemiring.toSemiring Set Set.instMembership associatedPrimes IsAssociatedPrime	—	—

IsAssociatedPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
annihilator_le 📖	mathematical	IsAssociatedPrime	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.annihilator Top.top Submodule Submodule.instTop	—	Submodule.bot_colon' LE.le.trans Submodule.annihilator_mono le_top Ideal.le_radical
eq_radical 📖	mathematical	Ideal.IsPrimary CommRing.toCommSemiring IsAssociatedPrime HasQuotient.Quotient Ideal CommSemiring.toSemiring Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule	Ideal.radical CommRing.toCommSemiring	—	Ideal.IsPrime.ne_top' Ideal.radical_top Submodule.colon_singleton_zero Ideal.instIsTwoSided_1 Ideal.Quotient.mkₐ_surjective Submodule.mem_colon_singleton Algebra.smul_def Ideal.Quotient.algebraMap_eq map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Submodule.mem_bot le_antisymm Ideal.radical_le_radical_iff Submodule.colon_univ Set.top_eq_univ Submodule.IsPrimary.mem_or_mem Ideal.radical_mono Ideal.mul_mem_right
isPrime 📖	mathematical	IsAssociatedPrime	Ideal.IsPrime CommSemiring.toSemiring	—	Submodule.IsAssociatedPrime.toIsPrime
map_of_injective 📖	mathematical	IsAssociatedPrime DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	IsAssociatedPrime	—	Submodule.IsAssociatedPrime.eq_radical_colon Submodule.IsAssociatedPrime.toIsPrime Ideal.ext SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass map_eq_zero_iff AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAssociatedPrime_iff 📖	mathematical	—	IsAssociatedPrime	—	RingHomInvPair.ids IsAssociatedPrime.map_of_injective injective

LinearEquiv.AssociatedPrimes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	mathematical	—	associatedPrimes	—	RingHomInvPair.ids le_antisymm associatedPrimes.subset_of_injective LinearEquiv.injective

Submodule

Definitions

Name	Category	Theorems
IsAssociatedPrime 📖	CompData	3 math math: isAssociatedPrime_def, isAssociatedPrime_iff, AssociatePrimes.mem_iff
associatedPrimes 📖	CompOp	7 math math: IsMinimalPrimaryDecomposition.comap_localized₀_eq_iInf, IsMinimalPrimaryDecomposition.mem_associatedPrimes, IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes, IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite, instIsPrimeValIdealMemSetAssociatedPrimes, AssociatePrimes.mem_iff, IsMinimalPrimaryDecomposition.mem_image_radical_colon_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsPrimeValIdealMemSetAssociatedPrimes 📖	mathematical	—	Ideal.IsPrime CommSemiring.toSemiring Ideal Set Set.instMembership associatedPrimes	—	IsAssociatedPrime.toIsPrime
isAssociatedPrime_def 📖	mathematical	—	IsAssociatedPrime Ideal.IsPrime CommSemiring.toSemiring Ideal.radical colon Set Set.instSingletonSet	—	IsAssociatedPrime.toIsPrime IsAssociatedPrime.eq_radical_colon
isAssociatedPrime_iff 📖	mathematical	—	IsAssociatedPrime Ideal.IsPrime CommSemiring.toSemiring colon Set Set.instSingletonSet	—	exists_eq_colon_of_mem_minimalPrimes Ideal.radical_minimalPrimes Ideal.minimalPrimes_eq_subsingleton_self Set.mem_singleton_iff Ideal.IsPrime.radical

Submodule.AssociatePrimes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_iff 📖	mathematical	—	Ideal CommSemiring.toSemiring Set Set.instMembership Submodule.associatedPrimes Submodule.IsAssociatedPrime	—	—

Submodule.IsAssociatedPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_radical_colon 📖	mathematical	Submodule.IsAssociatedPrime	Ideal.radical Submodule.colon CommSemiring.toSemiring Set Set.instSingletonSet	—	—
toIsPrime 📖	mathematical	Submodule.IsAssociatedPrime	Ideal.IsPrime CommSemiring.toSemiring	—	—

(root)

Definitions

Name	Category	Theorems
IsAssociatedPrime 📖	MathDef	8 math math: AssociatedPrimes.mem_iff, exists_le_isAssociatedPrime_of_isNoetherianRing, IsAssociatedPrime.map_of_injective, LinearEquiv.isAssociatedPrime_iff, AssociatePrimes.mem_iff, isAssociatedPrime_iff_exists_injective_linearMap, not_isAssociatedPrime_of_subsingleton, isAssociatedPrime_iff
associatedPrimes 📖	CompOp	21 math math: Module.associatedPrimes.mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule, AssociatedPrimes.mem_iff, Module.associatedPrimes.mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes, biUnion_associatedPrimes_eq_compl_regular, Module.associatedPrimes.preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule, instIsPrimeValIdealMemSetAssociatedPrimes, Ideal.IsMaximal.mem_associatedPrimes_of_isFractionRing, associatedPrimes.finite, biUnion_associatedPrimes_eq_zero_divisors, associatedPrimes.nonempty, associatedPrimes.subset_of_injective, associatedPrimes.eq_singleton_of_isPrimary, associatedPrimes.eq_empty_of_subsingleton, AssociatePrimes.mem_iff, associatedPrimes.prod, LinearEquiv.AssociatedPrimes.eq, Module.associatedPrimes.minimalPrimes_annihilator_subset_associatedPrimes, Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes, biUnion_associatedPrimes_eq_compl_nonZeroDivisors, associatedPrimes.subset_union_of_exact, Module.associatedPrimes.comap_mem_associatedPrimes_of_mem_associatedPrimes_of_isLocalizedModule_of_fg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biUnion_associatedPrimes_eq_compl_nonZeroDivisors 📖	mathematical	—	Set.iUnion Ideal CommSemiring.toSemiring Set Set.instMembership associatedPrimes NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.coe Submodule.setLike Compl.compl Set.instCompl Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Submonoid.instSetLike nonZeroDivisors	—	biUnion_associatedPrimes_eq_zero_divisors Set.ext
biUnion_associatedPrimes_eq_zero_divisors 📖	mathematical	—	Set.iUnion Ideal CommSemiring.toSemiring Set Set.instMembership associatedPrimes SetLike.coe Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule setOf AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Set.iUnion_congr_Prop subset_antisymm Set.instAntisymmSubset Set.iUnion₂_subset Ideal.IsPrime.ne_top exists_le_isAssociatedPrime_of_isNoetherianRing Set.mem_iUnion₂_of_mem isAssociatedPrime_iff Submodule.mem_colon_singleton
exists_le_isAssociatedPrime_of_isNoetherianRing 📖	mathematical	—	Ideal CommSemiring.toSemiring IsAssociatedPrime Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.colon Bot.bot Submodule Submodule.instBot Set Set.instSingletonSet	—	set_has_maximal_iff_noetherian Eq.le Submodule.mem_colon_singleton Submodule.mem_bot SMulCommClass.smul_comm smulCommClass_self smul_zero LE.le.eq_of_not_lt LE.le.trans smul_smul
instIsPrimeValIdealMemSetAssociatedPrimes 📖	mathematical	—	Ideal.IsPrime CommSemiring.toSemiring Ideal Set Set.instMembership associatedPrimes	—	Submodule.IsAssociatedPrime.toIsPrime
isAssociatedPrime_iff 📖	mathematical	—	IsAssociatedPrime Ideal.IsPrime CommSemiring.toSemiring Submodule.colon Bot.bot Submodule Submodule.instBot Set Set.instSingletonSet	—	Submodule.isAssociatedPrime_iff
isAssociatedPrime_iff_exists_injective_linearMap 📖	mathematical	—	IsAssociatedPrime CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ideal.IsPrime CommSemiring.toSemiring LinearMap RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule DFunLike.coe LinearMap.instFunLike	—	isAssociatedPrime_iff Eq.le LinearMap.ker_eq_bot Submodule.ker_liftQ_eq_bot' RingHomCompTriple.ids Submodule.ker_mkQ LinearMap.ker_comp_of_ker_eq_bot LinearMap.ker_eq_bot_of_injective Algebra.algebraMap_eq_smul_one one_smul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
not_isAssociatedPrime_of_subsingleton 📖	mathematical	—	IsAssociatedPrime	—	Ideal.IsPrime.ne_top Set.instReflSubset

associatedPrimes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_empty_of_subsingleton 📖	mathematical	—	associatedPrimes Set Ideal CommSemiring.toSemiring Set.instEmptyCollection	—	Set.ext not_isAssociatedPrime_of_subsingleton
eq_singleton_of_isPrimary 📖	mathematical	Ideal.IsPrimary CommRing.toCommSemiring	associatedPrimes CommRing.toCommSemiring HasQuotient.Quotient Ideal CommSemiring.toSemiring Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule Set Set.instSingletonSet Ideal.radical	—	Set.ext Set.mem_singleton_iff IsAssociatedPrime.eq_radical nonempty Ideal.instIsTwoSided_1 Ideal.Quotient.eq sub_zero Ideal.eq_top_iff_one
nonempty 📖	mathematical	—	Set.Nonempty Ideal CommSemiring.toSemiring associatedPrimes	—	exists_ne exists_le_isAssociatedPrime_of_isNoetherianRing
prod 📖	mathematical	—	associatedPrimes Prod.instAddCommMonoid Prod.instModule CommSemiring.toSemiring Set Ideal Set.instUnion	—	HasSubset.Subset.antisymm Set.instAntisymmSubset subset_union_of_exact LinearMap.inl_injective Function.Exact.inl_snd Set.union_subset_iff subset_of_injective LinearMap.inr_injective
subset_of_injective 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	Set Ideal CommSemiring.toSemiring Set.instHasSubset associatedPrimes	—	IsAssociatedPrime.map_of_injective
subset_union_of_exact 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Function.Exact AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Set Ideal CommSemiring.toSemiring Set.instHasSubset associatedPrimes Set.instUnion	—	le_antisymm Submodule.mem_colon_singleton Submodule.mem_bot map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass SMulCommClass.smul_comm smulCommClass_self smul_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Eq.ge Ideal.le_radical SemigroupAction.mul_smul Mathlib.Tactic.Contrapose.contrapose₁ Submonoid.mul_mem Submonoid.pow_mem Ideal.radical_mono RingHomSurjective.ids Function.Exact.linearMap_ker_eq LinearMap.mem_ker Mathlib.Tactic.Push.not_and_eq

---

← Back to Index