Exactness

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

Statistics

Metric	Count
Definitions	0
Theorems map_linearMap_of_isLocalization, of_isLocalized_maximal, bijective_of_isLocalization_isMaximal, bijective_of_isLocalization_of_span_eq_top, bijective_of_isLocalized_maximal, bijective_of_isLocalized_span, bijective_of_localized_maximal, bijective_of_localized_span, exact_of_isLocalized_maximal, exact_of_isLocalized_span, exact_of_localized_maximal, exact_of_localized_span, injective_of_isLocalization_isMaximal, injective_of_isLocalization_of_span_eq_top, injective_of_isLocalized_maximal, injective_of_isLocalized_span, injective_of_localized_maximal, injective_of_localized_span, surjective_of_isLocalization_isMaximal, surjective_of_isLocalization_of_span_eq_top, surjective_of_isLocalized_maximal, surjective_of_isLocalized_span, surjective_of_localized_maximal, surjective_of_localized_span	24
Total	24

IsLocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_linearMap_of_isLocalization 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike map Ideal.primeCompl Algebra.linearMap instIsLocalizedModuleLinearMapOfIsLocalization SemilinearMapClass.semilinearMap AlgHom IsScalarTower.toAlgHom AlgHom.funLike NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass linearMap_ext instIsLocalizedModuleLinearMapOfIsLocalization smulCommClass_self LinearMap.IsScalarTower.compatibleSMul' LinearMap.ext_ring RingHomCompTriple.ids map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_apply

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isLocalized_maximal 📖	mathematical	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.AtPrime LinearIndependent DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	LinearIndependent CommSemiring.toSemiring	—	Ideal.IsMaximal.isPrime' injective_of_isLocalized_maximal instIsLocalizedModuleFinsuppLinearMap instIsLocalizedModuleLinearMapOfIsLocalization smulCommClass_self LinearMap.CompatibleSMul.finsupp_dom LinearMap.IsScalarTower.compatibleSMul' IsLocalizedModule.map_linearCombination

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_of_isLocalization_isMaximal 📖	mathematical	IsScalarTower Algebra.toSMul CommSemiring.toSemiring IsLocalization.AtPrime Ideal.IsMaximal.isPrime' IsLocalizedModule.AtPrime NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SemilinearMapClass.semilinearMap AlgHom RingHom.id IsScalarTower.toAlgHom AlgHom.funLike NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Function.Bijective DFunLike.coe RingHom RingHom.instFunLike algebraMap	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	Ideal.IsMaximal.isPrime' NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass injective_of_isLocalization_isMaximal surjective_of_isLocalization_isMaximal
bijective_of_isLocalization_of_span_eq_top 📖	mathematical	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalization.Away Set Set.instMembership DFunLike.coe RingHom RingHom.instFunLike Function.Bijective IsLocalization.Away.map	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	—	injective_of_isLocalization_of_span_eq_top surjective_of_isLocalization_of_span_eq_top
bijective_of_isLocalized_maximal 📖	mathematical	IsLocalizedModule.AtPrime Ideal.IsMaximal.isPrime' Function.Bijective DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Ideal.primeCompl	Function.Bijective DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	Ideal.IsMaximal.isPrime' smulCommClass_self injective_of_isLocalized_maximal surjective_of_isLocalized_maximal
bijective_of_isLocalized_span 📖	mathematical	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule.Away Set Set.instMembership Function.Bijective DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Function.Bijective DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	smulCommClass_self injective_of_isLocalized_span surjective_of_isLocalized_span
bijective_of_localized_maximal 📖	mathematical	Function.Bijective LocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id Semiring.toNonAssocSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LocalizedModule.map	Function.Bijective DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	Ideal.IsMaximal.isPrime' smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 injective_of_localized_maximal surjective_of_localized_maximal
bijective_of_localized_span 📖	mathematical	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Function.Bijective LocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id OreLocalization.instAddCommMonoidOreLocalization Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Algebra.toModule LocalizedModule.map	Function.Bijective DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 injective_of_localized_span surjective_of_localized_span
exact_of_isLocalized_maximal 📖	mathematical	IsLocalizedModule.AtPrime Ideal.IsMaximal.isPrime' Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Ideal.primeCompl AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Ideal.IsMaximal.isPrime' smulCommClass_self RingHomSurjective.ids Submodule.eq_of_localization₀_maximal LinearMap.range_localizedMap_eq_localized₀_range LinearMap.ker_localizedMap_eq_localized₀_ker SetLike.ext_iff Submodule.ext
exact_of_isLocalized_span 📖	mathematical	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule.Away Set Set.instMembership Function.Exact DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	smulCommClass_self RingHomSurjective.ids Submodule.eq_of_isLocalized₀_span LinearMap.range_localizedMap_eq_localized₀_range LinearMap.ker_localizedMap_eq_localized₀_ker SetLike.ext_iff Submodule.ext
exact_of_localized_maximal 📖	mathematical	Function.Exact LocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id Semiring.toNonAssocSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LocalizedModule.map OreLocalization.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Ideal.IsMaximal.isPrime' smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 exact_of_isLocalized_maximal localizedModuleIsLocalizedModule
exact_of_localized_span 📖	mathematical	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Function.Exact LocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id OreLocalization.instAddCommMonoidOreLocalization Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Algebra.toModule LocalizedModule.map OreLocalization.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 exact_of_isLocalized_span localizedModuleIsLocalizedModule
injective_of_isLocalization_isMaximal 📖	mathematical	IsScalarTower Algebra.toSMul CommSemiring.toSemiring IsLocalization.AtPrime Ideal.IsMaximal.isPrime' IsLocalizedModule.AtPrime NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SemilinearMapClass.semilinearMap AlgHom RingHom.id IsScalarTower.toAlgHom AlgHom.funLike NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass DFunLike.coe RingHom RingHom.instFunLike algebraMap	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	Ideal.IsMaximal.isPrime' NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass injective_of_isLocalized_maximal instIsLocalizedModuleLinearMapOfIsLocalization smulCommClass_self LinearMap.IsScalarTower.compatibleSMul' DFunLike.coe_fn_eq IsLocalizedModule.map_linearMap_of_isLocalization
injective_of_isLocalization_of_span_eq_top 📖	mathematical	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalization.Away Set Set.instMembership DFunLike.coe RingHom RingHom.instFunLike IsLocalization.Away.map	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	—	IsScalarTower.of_algebraMap_eq' IsLocalization.Away.instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap IsScalarTower.of_algebraMap_eq Algebra.algebraMapSubmonoid_powers MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalization.map.congr_simp IsLocalization.map_eq injective_of_isLocalized_span instIsLocalizedModuleLinearMapOfIsLocalization instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid smulCommClass_self instIsLocalizationAlgebraMapSubmonoid Algebra.algebraMapSubmonoid_self Algebra.algebraMapSubmonoid_le_comap LinearMap.IsScalarTower.compatibleSMul' IsScalarTower.left IsScalarTower.right IsLocalization.map_linearMap_eq_toLinearMap_mapₐ
injective_of_isLocalized_maximal 📖	mathematical	IsLocalizedModule.AtPrime Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Ideal.primeCompl	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	Ideal.IsMaximal.isPrime' smulCommClass_self Module.eq_of_localization_maximal IsLocalizedModule.map_apply
injective_of_isLocalized_span 📖	mathematical	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule.Away Set Set.instMembership DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	smulCommClass_self Module.eq_of_isLocalized_span IsLocalizedModule.map_apply
injective_of_localized_maximal 📖	mathematical	LocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id Semiring.toNonAssocSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LocalizedModule.map	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	Ideal.IsMaximal.isPrime' smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 injective_of_isLocalized_maximal localizedModuleIsLocalizedModule
injective_of_localized_span 📖	mathematical	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule LocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id OreLocalization.instAddCommMonoidOreLocalization Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Algebra.toModule LocalizedModule.map	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 injective_of_isLocalized_span localizedModuleIsLocalizedModule
surjective_of_isLocalization_isMaximal 📖	mathematical	IsScalarTower Algebra.toSMul CommSemiring.toSemiring IsLocalization.AtPrime Ideal.IsMaximal.isPrime' IsLocalizedModule.AtPrime NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SemilinearMapClass.semilinearMap AlgHom RingHom.id IsScalarTower.toAlgHom AlgHom.funLike NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass DFunLike.coe RingHom RingHom.instFunLike algebraMap	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	Ideal.IsMaximal.isPrime' NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass surjective_of_isLocalized_maximal instIsLocalizedModuleLinearMapOfIsLocalization smulCommClass_self LinearMap.IsScalarTower.compatibleSMul' DFunLike.coe_fn_eq IsLocalizedModule.map_linearMap_of_isLocalization
surjective_of_isLocalization_of_span_eq_top 📖	mathematical	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalization.Away Set Set.instMembership DFunLike.coe RingHom RingHom.instFunLike IsLocalization.Away.map	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	—	IsScalarTower.of_algebraMap_eq' IsLocalization.Away.instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap IsScalarTower.of_algebraMap_eq Algebra.algebraMapSubmonoid_powers MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalization.map.congr_simp IsLocalization.map_eq surjective_of_isLocalized_span instIsLocalizedModuleLinearMapOfIsLocalization instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid smulCommClass_self instIsLocalizationAlgebraMapSubmonoid Algebra.algebraMapSubmonoid_self Algebra.algebraMapSubmonoid_le_comap LinearMap.IsScalarTower.compatibleSMul' IsScalarTower.left IsScalarTower.right IsLocalization.map_linearMap_eq_toLinearMap_mapₐ
surjective_of_isLocalized_maximal 📖	mathematical	IsLocalizedModule.AtPrime Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Ideal.primeCompl	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	Ideal.IsMaximal.isPrime' smulCommClass_self RingHomSurjective.ids LinearMap.range_eq_top Submodule.eq_top_of_localization₀_maximal LinearMap.range_localizedMap_eq_localized₀_range
surjective_of_isLocalized_span 📖	mathematical	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule.Away Set Set.instMembership DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	smulCommClass_self RingHomSurjective.ids LinearMap.range_eq_top Submodule.eq_top_of_isLocalized₀_span LinearMap.range_localizedMap_eq_localized₀_range
surjective_of_localized_maximal 📖	mathematical	LocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id Semiring.toNonAssocSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LocalizedModule.map	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	Ideal.IsMaximal.isPrime' smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 surjective_of_isLocalized_maximal localizedModuleIsLocalizedModule
surjective_of_localized_span 📖	mathematical	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule LocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id OreLocalization.instAddCommMonoidOreLocalization Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Algebra.toModule LocalizedModule.map	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 surjective_of_isLocalized_span localizedModuleIsLocalizedModule

---

← Back to Index