Module

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

Statistics

Metric	Count
Definitions mapEquiv, mapExtendScalars, extendScalarsOfIsLocalization, extendScalarsOfIsLocalizationEquiv, extendScalarsOfIsLocalization, extendScalarsOfIsLocalizationEquiv, map, localizationLocalization, ofIsLocalizedModule	9
Theorems linearIndependent_lift, mapEquiv_apply, mapEquiv_symm_apply, mapExtendScalars_apply_apply, map_bijective_iff_localizedModuleMap_bijective, map_injective_iff_localizedModuleMap_injective, map_surjective_iff_localizedModuleMap_surjective, extendScalarsOfIsLocalizationEquiv_apply, extendScalarsOfIsLocalizationEquiv_symm_apply, extendScalarsOfIsLocalization_apply, extendScalarsOfIsLocalization_symm_apply, iff_fractionRing, localization, localization_localization, of_isLocalizedModule, of_isLocalizedModule_of_isRegular, extendScalarsOfIsLocalizationEquiv_apply, extendScalarsOfIsLocalizationEquiv_symm_apply, extendScalarsOfIsLocalization_apply, extendScalarsOfIsLocalization_apply', restrictScalars_extendScalarsOfIsLocalization, coe_map_eq, map_id, map_injective, map_mk, map_surjective, restrictScalars_map_eq, localizationLocalization_apply, localizationLocalization_repr_algebraMap, localizationLocalization_span, ofIsLocalizedModule_apply, ofIsLocalizedModule_repr_apply, ofIsLocalizedModule_span, span_eq_top_localization_localization, span_eq_top_of_isLocalizedModule	35
Total	44

IsLocalizedModule

Definitions

Name	Category	Theorems
mapEquiv 📖	CompOp	2 math math: mapEquiv_apply, mapEquiv_symm_apply
mapExtendScalars 📖	CompOp	5 math math: mapExtendScalars_apply_apply, Module.FinitePresentation.linearEquivMapExtendScalars_apply, IsLocalization.mapExtendScalars_eq_toLinearMap_mapₐ, Module.FinitePresentation.isLocalizedModule_mapExtendScalars, Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearIndependent_lift 📖	—	LinearIndependent CommSemiring.toSemiring	—	—	isEmpty_or_nonempty linearIndependent_empty_type LinearIndependent.smul_left_injective linearIndependent_iff'ₛ IsRegular.right isRegular_of_smul_left_injective Finset.sum_congr SemigroupAction.mul_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass surj
mapEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike mapEquiv LinearMap LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module map LinearEquiv.toLinearMap	—	RingHomInvPair.ids
mapEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm mapEquiv LinearMap LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module map LinearEquiv.toLinearMap	—	RingHomInvPair.ids
mapExtendScalars_apply_apply 📖	mathematical	—	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 IsScalarTower.to_smulCommClass' mapExtendScalars map	—	smulCommClass_self IsScalarTower.to_smulCommClass'
map_bijective_iff_localizedModuleMap_bijective 📖	mathematical	—	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 map LocalizedModule Localization OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.instModule 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	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 RingHomInvPair.ids LocalizedModule.coe_map_eq
map_injective_iff_localizedModuleMap_injective 📖	mathematical	—	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 map LocalizedModule Localization OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.instModule 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	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 RingHomInvPair.ids LocalizedModule.coe_map_eq EquivLike.toEmbeddingLike
map_surjective_iff_localizedModuleMap_surjective 📖	mathematical	—	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 map LocalizedModule Localization OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.instModule 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	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 RingHomInvPair.ids LocalizedModule.coe_map_eq

LinearEquiv

Definitions

Name	Category	Theorems
extendScalarsOfIsLocalization 📖	CompOp	3 math math: extendScalarsOfIsLocalization_symm_apply, extendScalarsOfIsLocalizationEquiv_apply, extendScalarsOfIsLocalization_apply
extendScalarsOfIsLocalizationEquiv 📖	CompOp	2 math math: extendScalarsOfIsLocalizationEquiv_symm_apply, extendScalarsOfIsLocalizationEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extendScalarsOfIsLocalizationEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike Equiv.instEquivLike extendScalarsOfIsLocalizationEquiv extendScalarsOfIsLocalization	—	RingHomInvPair.ids
extendScalarsOfIsLocalizationEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike Equiv.instEquivLike Equiv.symm extendScalarsOfIsLocalizationEquiv restrictScalars	—	RingHomInvPair.ids
extendScalarsOfIsLocalization_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike extendScalarsOfIsLocalization	—	RingHomInvPair.ids
extendScalarsOfIsLocalization_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike symm extendScalarsOfIsLocalization	—	RingHomInvPair.ids

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_fractionRing 📖	mathematical	—	LinearIndependent CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	localization restrict_scalars faithfulSMul_iff_injective_smul_one IsScalarTower.right IsFractionRing.instFaithfulSMul
localization 📖	—	LinearIndependent CommSemiring.toSemiring	—	—	isLocalizedModule_id of_isLocalizedModule
localization_localization 📖	mathematical	LinearIndependent CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule	DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	of_isLocalizedModule instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid
of_isLocalizedModule 📖	mathematical	LinearIndependent CommSemiring.toSemiring	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	linearIndependent_iff'ₛ IsLocalizedModule.exists_of_eq Finset.sum_coe_sort DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr SemilinearMapClass.toMulActionSemiHomClass algebraMap_smul Finset.smul_sum smul_smul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Algebra.smul_def IsLocalization.map_units Zero.instNonempty Function.sometimes_spec IsLocalization.exist_integer_multiples
of_isLocalizedModule_of_isRegular 📖	mathematical	LinearIndependent CommSemiring.toSemiring IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike	—	map_injOn RingHomSurjective.ids Finsupp.range_linearCombination Finsupp.ext IsLocalizedModule.exists_of_eq IsRegular.left DFunLike.congr_fun SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass

LinearMap

Definitions

Name	Category	Theorems
extendScalarsOfIsLocalization 📖	CompOp	6 math math: extendScalarsOfIsLocalization_apply, extendScalarsOfIsLocalizationEquiv_apply, localized'_range_eq_range_localizedMap, localized'_ker_eq_ker_localizedMap, restrictScalars_extendScalarsOfIsLocalization, extendScalarsOfIsLocalization_apply'
extendScalarsOfIsLocalizationEquiv 📖	CompOp	2 math math: extendScalarsOfIsLocalizationEquiv_apply, extendScalarsOfIsLocalizationEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extendScalarsOfIsLocalizationEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap addCommMonoid module IsScalarTower.to_smulCommClass smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike extendScalarsOfIsLocalizationEquiv extendScalarsOfIsLocalization	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass smulCommClass_self
extendScalarsOfIsLocalizationEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm extendScalarsOfIsLocalizationEquiv restrictScalars	—	RingHomInvPair.ids smulCommClass_self IsScalarTower.to_smulCommClass
extendScalarsOfIsLocalization_apply 📖	mathematical	—	extendScalarsOfIsLocalization restrictScalars CommSemiring.toSemiring IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul	—	IsScalarTower.compatibleSMul
extendScalarsOfIsLocalization_apply' 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike extendScalarsOfIsLocalization	—	—
restrictScalars_extendScalarsOfIsLocalization 📖	mathematical	—	restrictScalars CommSemiring.toSemiring IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul extendScalarsOfIsLocalization	—	IsScalarTower.compatibleSMul

LocalizedModule

Definitions

Name	Category	Theorems
map 📖	CompOp	12 math math: restrictScalars_map_eq, Module.FinitePresentation.exists_notMem_bijective, map_surjective, IsLocalizedModule.map_surjective_iff_localizedModuleMap_surjective, map_injective, coe_map_eq, IsLocalizedModule.map_bijective_iff_localizedModuleMap_bijective, map_id, IsLocalizedModule.map_injective_iff_localizedModuleMap_injective, exists_bijective_map_powers, map_mk, instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_map_eq 📖	mathematical	—	DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.oreSetComm RingHom.id Semiring.toNonAssocSemiring LocalizedModule 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 map LinearEquiv RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm IsLocalizedModule.iso IsLocalizedModule.map	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 RingHomInvPair.ids LinearMap.IsScalarTower.compatibleSMul LinearMap.coe_restrictScalars RingHomCompTriple.ids restrictScalars_map_eq
map_id 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule 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 LinearMap.instFunLike map LinearMap.id	—	LinearMap.ext smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 LinearMap.congr_fun localizedModuleIsLocalizedModule IsLocalizedModule.map_id
map_injective 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	LocalizedModule Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule 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 map	—	IsLocalizedModule.map_injective IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule
map_mk 📖	mathematical	—	DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.oreSetComm RingHom.id Semiring.toNonAssocSemiring LocalizedModule 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 map	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 localizedModuleIsLocalizedModule IsLocalizedModule.mk_eq_mk' IsLocalizedModule.map_mk'
map_surjective 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	LocalizedModule Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule 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 map	—	IsLocalizedModule.map_surjective IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule
restrictScalars_map_eq 📖	mathematical	—	LinearMap.restrictScalars Localization CommSemiring.toCommMonoid LocalizedModule CommSemiring.toSemiring OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id OreLocalization.instModule LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid Monoid.toMulAction Algebra.toSMul OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike map LinearMap.comp RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm IsLocalizedModule.iso IsLocalizedModule.map	—	IsScalarTower.left IsScalarTower.right LinearMap.IsScalarTower.compatibleSMul OreLocalization.instIsScalarTower_1 smulCommClass_self IsScalarTower.to_smulCommClass' RingHomCompTriple.ids RingHomInvPair.ids LinearEquiv.eq_toLinearMap_symm_comp LinearEquiv.comp_toLinearMap_symm_eq IsLocalizedModule.linearMap_ext LinearMap.comp_assoc IsLocalizedModule.iso_symm_comp LinearMap.ext IsLocalizedModule.iso_mk_one IsLocalizedModule.map_apply

Module.Basis

Definitions

Name	Category	Theorems
localizationLocalization 📖	CompOp	7 math math: Algebra.map_leftMulMatrix_localization, Algebra.traceMatrix_localizationLocalization, localizationLocalization_apply, localizationLocalization_repr_algebraMap, localizationLocalization_span, Algebra.discr_localizationLocalization, FractionalIdeal.abs_det_basis_change
ofIsLocalizedModule 📖	CompOp	3 math math: ofIsLocalizedModule_apply, ofIsLocalizedModule_span, ofIsLocalizedModule_repr_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
localizationLocalization_apply 📖	mathematical	—	DFunLike.coe Module.Basis CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instFunLike localizationLocalization RingHom RingHom.instFunLike algebraMap	—	ofIsLocalizedModule_apply instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid
localizationLocalization_repr_algebraMap 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.instAddCommMonoid Algebra.toModule Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike repr localizationLocalization RingHom RingHom.instFunLike algebraMap	—	ofIsLocalizedModule_repr_apply instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid
localizationLocalization_span 📖	mathematical	—	Submodule.span CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Set.range DFunLike.coe Module.Basis instFunLike localizationLocalization LinearMap.range RingHom.id RingHomSurjective.ids SemilinearMapClass.semilinearMap AlgHom IsScalarTower.toAlgHom AlgHom.funLike NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass	—	ofIsLocalizedModule_span instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid
ofIsLocalizedModule_apply 📖	mathematical	—	DFunLike.coe Module.Basis CommSemiring.toSemiring instFunLike ofIsLocalizedModule LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	ofIsLocalizedModule.eq_1
ofIsLocalizedModule_repr_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike repr ofIsLocalizedModule LinearMap LinearMap.instFunLike RingHom RingHom.instFunLike algebraMap	—	RingHomCompTriple.ids LinearMap.CompatibleSMul.finsupp_cod LinearMap.IsScalarTower.compatibleSMul IsScalarTower.right RingHomInvPair.ids ext LinearMap.coe_comp LinearMap.coe_restrictScalars LinearEquiv.coe_coe ofIsLocalizedModule_apply repr_self LinearMap.map_zero Finsupp.mapRange.linearMap_apply Finsupp.mapRange_single Algebra.linearMap_apply map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass DFunLike.congr_fun LinearMap.congr_fun
ofIsLocalizedModule_span 📖	mathematical	—	Submodule.span CommSemiring.toSemiring Set.range DFunLike.coe Module.Basis instFunLike ofIsLocalizedModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids	—	RingHomSurjective.ids Set.ext ofIsLocalizedModule_apply Submodule.map_span span_eq Submodule.map_top

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
span_eq_top_localization_localization 📖	mathematical	Submodule.span CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Top.top Submodule Submodule.instTop	Set.image DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	span_eq_top_of_isLocalizedModule instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid
span_eq_top_of_isLocalizedModule 📖	mathematical	Submodule.span CommSemiring.toSemiring Top.top Submodule Submodule.instTop	Set.image DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	top_unique IsLocalizedModule.surj IsLocalization.map_units Submodule.smul_mem Submodule.span_subset_span LinearMap.IsScalarTower.compatibleSMul IsScalarTower.left LinearMap.coe_restrictScalars RingHomSurjective.ids LinearMap.map_span Submodule.mem_map_of_mem Submodule.mem_top inv_smul_eq_iff Units.smul_isUnit algebraMap_smul Submonoid.smul_def

---

← Back to Index