Localization

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

Statistics

Metric	Count
Definitions	0
Theorems comap_mem_associatedPrimes_of_mem_associatedPrimes_of_isLocalizedModule_of_fg, mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes, mem_associatedPrimes_atPrime_of_mem_associatedPrimes, mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule, minimalPrimes_annihilator_subset_associatedPrimes, preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule	6
Total	6

Module.associatedPrimes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_mem_associatedPrimes_of_mem_associatedPrimes_of_isLocalizedModule_of_fg 📖	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership associatedPrimes AddCommGroup.toAddCommMonoid Ideal.FG Ideal.comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass	—	—	RingHom.instRingHomClass IsLocalizedModule.mk'_surjective Ideal.subset_span Ideal.IsPrime.under le_antisymm Ideal.span_le SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass Finset.dvd_prod_of_mem Finset.mem_univ Submonoid.coe_mul smul_smul mul_assoc mul_comm smul_eq_zero_of_right Ideal.comap.congr_simp algebraMap_smul IsLocalizedModule.mk'.congr_simp IsLocalizedModule.mk'_zero Set.disjoint_left IsLocalization.disjoint_comap_iff Ideal.IsPrime.ne_top' Ideal.IsPrime.mul_mem_iff_mem_or_mem Ideal.instIsTwoSided_1 IsLocalizedModule.mk'_eq_zero'
mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership associatedPrimes AddCommGroup.toAddCommMonoid	Localization.AtPrime OreLocalization.instCommSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid LocalizedModule.AtPrime OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule IsLocalRing.maximalIdeal Localization.AtPrime.isLocalRing	—	mem_associatedPrimes_atPrime_of_mem_associatedPrimes
mem_associatedPrimes_atPrime_of_mem_associatedPrimes 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership associatedPrimes AddCommGroup.toAddCommMonoid	Localization.AtPrime OreLocalization.instCommSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid LocalizedModule.AtPrime OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule IsLocalRing.maximalIdeal Localization.AtPrime.isLocalRing	—	mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule Localization.isLocalization IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule OreLocalization.instIsScalarTower_1 Localization.AtPrime.isLocalRing RingHom.instRingHomClass Localization.AtPrime.comap_maximalIdeal
mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule 📖	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership associatedPrimes AddCommGroup.toAddCommMonoid Ideal.comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass	—	—	RingHom.instRingHomClass IsLocalization.isPrime_iff_isPrime_disjoint IsLocalization.disjoint_comap_iff Ideal.comap.congr_simp Ideal.comap_top Ideal.ext IsLocalization.exists_mk'_eq IsLocalizedModule.mk'_one Submodule.mem_colon_singleton Submodule.mem_bot IsLocalizedModule.mk'_smul_mk' mul_one IsLocalizedModule.mk'_eq_zero' one_smul IsLocalization.mk'_one sub_eq_zero IsLocalization.mk'_mul IsLocalization.mk'_sub IsLocalization.mk'.congr_simp sub_self one_mul IsLocalization.mk'_zero Ideal.IsTwoSided.mul_mem_of_left Ideal.instIsTwoSided_1 smul_smul Submonoid.coe_mul SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass mul_comm Ideal.mem_comap
minimalPrimes_annihilator_subset_associatedPrimes 📖	mathematical	—	Set Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set.instHasSubset Ideal.minimalPrimes Module.annihilator AddCommGroup.toAddCommMonoid associatedPrimes	—	PrimeSpectrum.isPrime Module.mem_support_iff Module.support_eq_zeroLocus instIsConcreteLE associatedPrimes.nonempty IsLocalization.instIsNoetherianRingLocalization IsAssociatedPrime.isPrime RingHom.instRingHomClass Submodule.annihilator_top IsAssociatedPrime.annihilator_le preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule Localization.isLocalization IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule OreLocalization.instIsScalarTower_1 IsLocalization.disjoint_comap_iff Ideal.IsPrime.ne_top Ideal.one_notMem Minimal.eq_of_le Membership.mem.out
preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule 📖	mathematical	—	Set.preimage Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass associatedPrimes AddCommGroup.toAddCommMonoid	—	Set.ext RingHom.instRingHomClass mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule comap_mem_associatedPrimes_of_mem_associatedPrimes_of_isLocalizedModule_of_fg isNoetherianRing_iff_ideal_fg

---

← Back to Index