Submodule

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

Statistics

Metric	Count
Definitions	0
Theorems eq_of_localization_maximal, eq_of_isLocalized_span, eq_of_localization_maximal, eq_zero_of_isLocalized_span, eq_zero_of_localization_maximal, subsingleton_of_localization_maximal, eq_bot_of_isLocalized'_span, eq_bot_of_isLocalized₀_span, eq_bot_of_localization_maximal, eq_bot_of_localization₀_maximal, eq_of_isLocalized'_span, eq_of_isLocalized₀_span, eq_of_localization_maximal, eq_of_localization₀_maximal, eq_top_of_isLocalized'_span, eq_top_of_isLocalized₀_span, eq_top_of_localization_maximal, eq_top_of_localization₀_maximal, le_of_isLocalized_span, le_of_localization_maximal, mem_of_isLocalized_span, mem_of_localization_maximal	22
Total	22

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_localization_maximal 📖	—	IsLocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike IsLocalizedModule.map	—	—	Ideal.IsMaximal.isPrime' smulCommClass_self ext Module.eq_of_localization_maximal IsLocalizedModule.map_apply DFunLike.congr_fun

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_isLocalized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike	—	—	Ideal.exists_disjoint_powers_of_span_eq_top IsLocalizedModule.eq_iff_exists Set.disjoint_left one_smul Ideal.eq_top_iff_one
eq_of_localization_maximal 📖	—	IsLocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	—	Ideal.IsMaximal.isPrime' one_smul Ideal.exists_le_maximal Ideal.ne_top_iff_one IsLocalizedModule.eq_iff_exists
eq_zero_of_isLocalized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—	eq_of_isLocalized_span map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
eq_zero_of_localization_maximal 📖	—	IsLocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—	Ideal.IsMaximal.isPrime' eq_of_localization_maximal map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
subsingleton_of_localization_maximal 📖	—	IsLocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime'	—	—	Ideal.IsMaximal.isPrime' eq_of_localization_maximal

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_bot_of_isLocalized'_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal 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 localized' Bot.bot Submodule instBot	—	—	eq_of_isLocalized'_span localized'_bot
eq_bot_of_isLocalized₀_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership localized₀ Bot.bot Submodule instBot	—	—	eq_of_isLocalized₀_span localized₀_bot
eq_bot_of_localization_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 localized' Bot.bot Submodule instBot	—	—	Ideal.IsMaximal.isPrime' eq_of_localization_maximal localized'_bot
eq_bot_of_localization₀_maximal 📖	—	IsLocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' localized₀ Bot.bot Submodule instBot	—	—	Ideal.IsMaximal.isPrime' eq_of_localization₀_maximal localized₀_bot
eq_of_isLocalized'_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal 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 localized'	—	—	eq_of_isLocalized₀_span
eq_of_isLocalized₀_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership localized₀	—	—	le_antisymm le_of_isLocalized_span Eq.le Eq.ge
eq_of_localization_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 localized'	—	—	Ideal.IsMaximal.isPrime' eq_of_localization₀_maximal
eq_of_localization₀_maximal 📖	—	IsLocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' localized₀	—	—	Ideal.IsMaximal.isPrime' le_antisymm le_of_localization_maximal Eq.le Eq.ge
eq_top_of_isLocalized'_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal 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 localized' Submodule	—	—	eq_of_isLocalized'_span localized'_top
eq_top_of_isLocalized₀_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership localized₀ Submodule	—	—	eq_of_isLocalized₀_span localized₀_top
eq_top_of_localization_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 localized' Top.top Submodule instTop	—	—	Ideal.IsMaximal.isPrime' eq_of_localization_maximal localized'_top
eq_top_of_localization₀_maximal 📖	—	IsLocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' localized₀ Top.top Submodule instTop	—	—	Ideal.IsMaximal.isPrime' eq_of_localization₀_maximal localized₀_top
le_of_isLocalized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder localized₀	—	—	mem_of_isLocalized_span IsLocalizedModule.mk'_one
le_of_localization_maximal 📖	—	IsLocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder localized₀	—	—	Ideal.IsMaximal.isPrime' mem_of_localization_maximal IsLocalizedModule.mk'_one
mem_of_isLocalized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership Submodule SetLike.instMembership setLike localized₀ DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike	—	—	Ideal.exists_disjoint_powers_of_span_eq_top IsLocalizedModule.mk'_eq_mk'_iff IsLocalizedModule.mk'_one Set.disjoint_right smul_mem smul_smul one_smul Ideal.eq_top_iff_one
mem_of_localization_maximal 📖	—	IsLocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' Submodule SetLike.instMembership setLike localized₀ DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	—	Ideal.IsMaximal.isPrime' Not.imp_symm Ideal.exists_le_maximal IsLocalizedModule.mk'_eq_mk'_iff IsLocalizedModule.mk'_one smul_mem smul_smul one_smul Ideal.eq_top_iff_one

---

← Back to Index