Finiteness

📁 Source: Mathlib/RingTheory/Localization/Finiteness.lean

Statistics

Metric	Count
Definitions	0
Theorems fg_of_localizationSpan, instLocalizationLocalizedModule, of_isLocalizedModule, of_localizationSpan, of_localizationSpan', of_localizationSpan_finite, of_localizationSpan_finite', ker_fg_of_localizationSpan	8
Total	8

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg_of_localizationSpan 📖	—	span CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule FG Localization.Away CommRing.toCommMonoid Set Set.instMembership OreLocalization.instSemiring Ring.toSemiring CommRing.toRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm map RingHom RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id	—	—	Module.Finite.iff_fg IsScalarTower.right Module.Finite.of_localizationSpan' Localization.isLocalization Submodule.isScalarTower' Algebra.idealMap_isLocalizedModule Module.Finite.of_fg

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLocalizationLocalizedModule 📖	mathematical	—	Module.Finite Localization CommSemiring.toCommMonoid LocalizedModule OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule	—	of_isLocalizedModule Localization.isLocalization IsScalarTower.left IsScalarTower.right OreLocalization.instIsScalarTower_1 localizedModuleIsLocalizedModule
of_isLocalizedModule 📖	mathematical	—	Module.Finite CommSemiring.toSemiring	—	Finset.coe_image span_eq_top_of_isLocalizedModule
of_localizationSpan 📖	—	Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Module.Finite Localization.Away CommRing.toCommMonoid Set Set.instMembership LocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.instSemiring Ring.toSemiring CommRing.toRing CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModule	—	—	IsScalarTower.left IsScalarTower.right of_localizationSpan' Localization.isLocalization OreLocalization.instIsScalarTower_1 localizedModuleIsLocalizedModule
of_localizationSpan' 📖	—	Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalization.Away Set Set.instMembership IsScalarTower Algebra.toSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsLocalizedModule Submonoid.powers Module.Finite	—	—	Ideal.span_eq_top_iff_finite of_localizationSpan_finite'
of_localizationSpan_finite 📖	—	Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring SetLike.coe Finset Finset.instSetLike Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Module.Finite Localization.Away CommRing.toCommMonoid SetLike.instMembership LocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.instSemiring Ring.toSemiring CommRing.toRing CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModule	—	—	IsScalarTower.left IsScalarTower.right of_localizationSpan_finite' Localization.isLocalization OreLocalization.instIsScalarTower_1 localizedModuleIsLocalizedModule
of_localizationSpan_finite' 📖	—	Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring SetLike.coe Finset Finset.instSetLike Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalization.Away SetLike.instMembership IsScalarTower Algebra.toSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsLocalizedModule Submonoid.powers Module.Finite	—	—	Submodule.span_attach_biUnion eq_top_iff Submodule.mem_of_span_eq_top_of_smul_pow_mem multiple_mem_span_of_mem_localization_span IsLocalizedModule.smul_mem_finsetIntegerMultiple_span IsLocalizedModule.mk'_one IsLocalizedModule.mk'_smul Submonoid.smul_def le_iSup pow_add SemigroupAction.mul_smul fg_top

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_fg_of_localizationSpan 📖	—	Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.FG Localization.Away CommSemiring.toCommMonoid Set Set.instMembership OreLocalization.instSemiring Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm ker DFunLike.coe RingHom instFunLike instRingHomClass Localization.awayMap	—	—	instRingHomClass Ideal.fg_of_localizationSpan Localization.isLocalization MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Submonoid.le_comap_map Submonoid.map_powers IsLocalization.ker_map

---

← Back to Index