Semilocal

📁 Source: Mathlib/RingTheory/LocalProperties/Semilocal.lean

Statistics

Metric	Count
Definitions	0
Theorems of_isLocalization_maximal, of_isLocalized_maximal, of_localized_maximal, fg_of_isLocalized_maximal, fg_of_localized_maximal, isPrincipalIdealRing_of_isPrincipalIdealRing_isLocalization_maximal	6
Total	6

IsNoetherianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isLocalization_maximal 📖	—	IsLocalization.AtPrime Ideal.IsMaximal.isPrime' IsNoetherianRing CommSemiring.toSemiring	—	—	Ideal.IsMaximal.isPrime' Submodule.fg_of_isLocalized_maximal IsScalarTower.right instIsLocalizedModuleLinearMapOfIsLocalization IsNoetherian.noetherian

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isLocalized_maximal 📖	—	IsLocalization.AtPrime Ideal.IsMaximal.isPrime' IsScalarTower Algebra.toSMul CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsLocalizedModule Ideal.primeCompl Module.Finite	—	—	Ideal.IsMaximal.isPrime' MaximalSpectrum.isMaximal Submodule.eq_top_of_localization_maximal eq_top_iff Submodule.localized'_span Submodule.span_le CanLift.prf Finset.FinsetCoe.canLift SetLike.mem_coe IsLocalization.smul_mem_iff Submodule.subset_span Finset.coe_biUnion Set.iUnion_congr_Prop Finset.coe_univ Finset.coe_image Set.iUnion_true IsLocalizedModule.surj fg_top
of_localized_maximal 📖	—	Module.Finite Localization CommSemiring.toCommMonoid Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' LocalizedModule OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule	—	—	Ideal.IsMaximal.isPrime' of_isLocalized_maximal Localization.isLocalization IsScalarTower.left IsScalarTower.right OreLocalization.instIsScalarTower_1 localizedModuleIsLocalizedModule

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg_of_isLocalized_maximal 📖	—	IsLocalization.AtPrime Ideal.IsMaximal.isPrime' IsScalarTower Algebra.toSMul CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsLocalizedModule Ideal.primeCompl FG localized'	—	—	Ideal.IsMaximal.isPrime' Module.Finite.of_isLocalized_maximal isScalarTower' IsScalarTower.left isLocalizedModule
fg_of_localized_maximal 📖	—	FG Localization CommSemiring.toCommMonoid Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' LocalizedModule OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule localized	—	—	Ideal.IsMaximal.isPrime' fg_of_isLocalized_maximal Localization.isLocalization IsScalarTower.left IsScalarTower.right OreLocalization.instIsScalarTower_1 localizedModuleIsLocalizedModule

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrincipalIdealRing_of_isPrincipalIdealRing_isLocalization_maximal 📖	—	IsLocalization.AtPrime CommRing.toCommSemiring Ideal.IsMaximal.isPrime' IsPrincipalIdealRing CommSemiring.toSemiring	—	—	Ideal.IsMaximal.isPrime' IsNoetherianRing.of_isLocalization_maximal isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing Module.Finite.self IsIntegrallyClosed.of_isLocalization_maximal IsLocalization.isDomain_of_atPrime IsDedekindDomainDvr.isIntegrallyClosed IsDedekindDomain.isDedekindDomainDvr IsPrincipalIdealRing.isDedekindDomain Ring.krullDimLE_of_isLocalization_maximal IsPrincipalIdealRing.krullDimLE_one Ring.krullDimLE_one_iff_of_noZeroDivisors IsDomain.to_noZeroDivisors MaximalSpectrum.range_asIdeal Set.finite_range IsPrincipalIdealRing.of_finite_maximals

---

← Back to Index