Finiteness

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

Statistics

Metric	Count
Definitions	0
Theorems fg_of_localizationSpan, smul_mem_finsetIntegerMultiple_span, instAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, instFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors, instLocalizationLocalizedModule, of_isLocalization, of_isLocalizedModule, of_localizationSpan, of_localizationSpan', of_localizationSpan_finite, of_localizationSpan_finite', ker_fg_of_localizationSpan, multiple_mem_adjoin_of_mem_localization_adjoin, multiple_mem_span_of_mem_localization_span	14
Total	14

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg_of_localizationSpan 📖	mathematical	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	FG CommSemiring.toSemiring CommRing.toCommSemiring	—	Module.Finite.iff_fg IsScalarTower.right Module.Finite.of_localizationSpan' Localization.isLocalization Submodule.isScalarTower' Algebra.idealMap_isLocalizedModule Module.Finite.of_fg

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_mem_finsetIntegerMultiple_span 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule SetLike.instMembership Submodule.setLike Submodule.span SetLike.coe Finset Finset.instSetLike DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Submodule.setLike Submodule.span SetLike.coe Finset Finset.instSetLike finsetIntegerMultiple Submonoid.map RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap Submonoid.smul Algebra.toSMul	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Algebra.algebraMap_eq_smul_one smul_assoc finsetIntegerMultiple_image Subtype.prop Set.isScalarTower one_smul smulCommClass_self Set.smul_mem_smul_set RingHomSurjective.ids Submodule.map_span AlgHom.coe_toLinearMap Algebra.linearMap_apply map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Submodule.span_smul eq_iff_exists Submonoid.smul_def Submonoid.coe_mul smul_smul Algebra.smul_def Submodule.smul_mem

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl 📖	mathematical	—	Module.Finite Localization.AtPrime CommRing.toCommSemiring Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommSemiring.toSemiring Ideal.primeCompl OreLocalization.instSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instAddCommMonoidOreLocalization CommMonoid.toMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule Algebra.toModule OreLocalization.instCommSemiring instAlgebraLocalizationAlgebraMapSubmonoid	—	of_isLocalization OreLocalization.instIsScalarTower IsScalarTower.right instIsScalarTowerLocalizationAlgebraMapSubmonoid Localization.isLocalization
instFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors 📖	mathematical	—	Module.Finite FractionRing Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommRing.toCommSemiring CommSemiring.toSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization CommMonoid.toMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule Algebra.toModule OreLocalization.instCommSemiring instAlgebraLocalizationAlgebraMapSubmonoid	—	IsScalarTower.right instIsScalarTowerLocalizationAlgebraMapSubmonoid of_isLocalization OreLocalization.instIsScalarTower Localization.isLocalization
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_isLocalization 📖	mathematical	—	Module.Finite CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule	—	Submonoid.le_comap_map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalization.ringHom_ext IsLocalization.map_comp Finset.coe_image span_eq_top_localization_localization
of_isLocalizedModule 📖	mathematical	—	Module.Finite CommSemiring.toSemiring	—	Finset.coe_image span_eq_top_of_isLocalizedModule
of_localizationSpan 📖	mathematical	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	Module.Finite CommSemiring.toSemiring CommRing.toCommSemiring	—	IsScalarTower.left IsScalarTower.right of_localizationSpan' Localization.isLocalization OreLocalization.instIsScalarTower_1 localizedModuleIsLocalizedModule
of_localizationSpan' 📖	mathematical	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	Module.Finite CommSemiring.toSemiring CommRing.toCommSemiring	—	Ideal.span_eq_top_iff_finite of_localizationSpan_finite'
of_localizationSpan_finite 📖	mathematical	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	Module.Finite CommSemiring.toSemiring CommRing.toCommSemiring	—	IsScalarTower.left IsScalarTower.right of_localizationSpan_finite' Localization.isLocalization OreLocalization.instIsScalarTower_1 localizedModuleIsLocalizedModule
of_localizationSpan_finite' 📖	mathematical	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	Module.Finite CommSemiring.toSemiring CommRing.toCommSemiring	—	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 📖	mathematical	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	Ideal.FG CommSemiring.toSemiring CommRing.toCommSemiring ker RingHom Semiring.toNonAssocSemiring instFunLike instRingHomClass	—	instRingHomClass Ideal.fg_of_localizationSpan Localization.isLocalization MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Submonoid.le_comap_map Submonoid.map_powers IsLocalization.ker_map

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
multiple_mem_adjoin_of_mem_localization_adjoin 📖	mathematical	Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike Subalgebra Subalgebra.instSetLike Algebra.adjoin Submonoid.smul Algebra.toSMul	—	Algebra.adjoin_eq_span multiple_mem_span_of_mem_localization_span
multiple_mem_span_of_mem_localization_span 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike Submodule.span	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike Submodule Submodule.setLike Submodule.span Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Submodule.mem_span_finite_of_mem_span Finset.induction_on Finset.coe_empty Submodule.span_empty one_smul Finset.coe_insert IsLocalization.surj Submodule.smul_mem smul_add smul_smul SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass mul_comm algebraMap_smul Algebra.smul_def smul_assoc Submodule.span_mono

---

← Back to Index