Basic

📁 Source: Mathlib/Algebra/Module/LocalizedModule/Basic.lean

Statistics

Metric	Count
Definitions IsLocalizedModule, fromLocalizedModule, fromLocalizedModule', iso, liftOfLE, linearEquiv, map, mk', algebra', algebraOfIsLocalization, divBy, instCommRing, instCommSemiring, instMonoid, instRing, instSemiring, lift', liftOfLE, liftOn, liftOn₂, mk, mkLinearMap, moduleOfIsLocalization, mul, numeratorRingHom, r, setoid, smulOfIsLocalization	28
Theorems eq_iff_exists, eq_zero_iff, exists_of_eq, ext, fromLocalizedModule'_add, fromLocalizedModule'_mk, fromLocalizedModule'_smul, bij, inj, surj, fromLocalizedModule_mk, injective_iff_isRegular, injective_of_map_eq, injective_of_map_zero, instIsTorsionFreeLocalizationLocalizedModuleOfIsDomain, instLiftOfLE, isRegular_of_smul_left_injective, isScalarTower_module, isTorsionFree, isTorsionFree_of_forall_isRegular, is_universal, iso_apply_mk, iso_localizedModule_eq_refl, iso_mk_one, iso_symm_apply, iso_symm_apply', iso_symm_apply_aux, iso_symm_comp, liftOfLE_apply, liftOfLE_comp, liftOfLE_mk', lift_apply, lift_comp, lift_comp_iso, lift_iso, lift_unique, linearEquiv_apply, linearEquiv_symm_apply, linearMap_ext, map_LocalizedModules, map_apply, map_comp, map_comp', map_id, map_injective, map_iso_commute, map_mk', map_surjective, map_units, mem_ker_iff, mk'_add, mk'_add_mk', mk'_cancel, mk'_cancel', mk'_cancel_left, mk'_cancel_right, mk'_eq_iff, mk'_eq_mk'_iff, mk'_eq_zero, mk'_eq_zero', mk'_mul_mk', mk'_mul_mk'_of_map_mul, mk'_neg, mk'_one, mk'_smul, mk'_smul_mk', mk'_sub, mk'_sub_mk', mk'_surjective, mk'_zero, mkOfAlgebra, mk_eq_mk', of_exists_mul_mem, of_linearEquiv, of_linearEquiv_right, of_restrictScalars, smul_inj, smul_injective, subsingleton_iff, subsingleton_iff_ker_eq_top, subsingleton_of_subsingleton, surj, surj', algebraMap_mk, algebraMap_mk', divBy_apply, divBy_mul_by, eq_zero_of_smul_eq_zero, induction_on, induction_on₂, instIsScalarTower, instSubsingleton, lift'_add, lift'_mk, lift'_smul, liftOn_mk, liftOn₂_mk, lift_comp, lift_mk, lift_mk_one, lift_unique, mem_ker_mkLinearMap_iff, mk'_smul_mk, mkLinearMap_apply, mk_add_mk, mk_cancel, mk_cancel_common_left, mk_cancel_common_right, mk_eq, mk_mul_mk, mk_mul_mk', mk_neg, mk_smul_mk, mul_by_divBy, mul_smul', oreEqv_eq_r, isEquiv, smul'_mk, smul'_mul, smul_def, smul_eq_iff_of_mem, subsingleton, subsingleton_iff, subsingleton_iff_ker_eq_top, zero_mk, isLocalizedModule_id, isLocalizedModule_iff, localizedModuleIsLocalizedModule	128
Total	156

IsLocalizedModule

Definitions

Name	Category	Theorems
fromLocalizedModule 📖	CompOp	4 math math: fromLocalizedModule.bij, fromLocalizedModule.inj, fromLocalizedModule_mk, fromLocalizedModule.surj
fromLocalizedModule' 📖	CompOp	3 math math: fromLocalizedModule'_add, fromLocalizedModule'_mk, fromLocalizedModule'_smul
iso 📖	CompOp	12 math math: iso_symm_apply', LocalizedModule.restrictScalars_map_eq, iso_symm_apply, iso_apply_mk, iso_symm_comp, LocalizedModule.coe_map_eq, lift_comp_iso, iso_symm_apply_aux, iso_localizedModule_eq_refl, map_iso_commute, lift_iso, iso_mk_one
liftOfLE 📖	CompOp	4 math math: instLiftOfLE, liftOfLE_apply, liftOfLE_comp, liftOfLE_mk'
linearEquiv 📖	CompOp	2 math math: linearEquiv_apply, linearEquiv_symm_apply
map 📖	CompOp	35 math math: LocalizedModule.restrictScalars_map_eq, LinearMap.ker_localizedMap_eq_localized'_ker, LinearMap.ker_localizedMap_eq_localized₀_ker, map_linearMap_of_isLocalization, map_surjective_iff_localizedModuleMap_surjective, LinearMap.toKerLocalized_isLocalizedModule, Module.FinitePresentation.linearEquivMap_symm_apply, LinearMap.localized'_range_eq_range_localizedMap, LinearMap.localized'_ker_eq_ker_localizedMap, mapExtendScalars_apply_apply, map_comp', LocalizedModule.coe_map_eq, map_linearCombination, mapEquiv_apply, map_injective, Module.FinitePresentation.linearEquivMap_apply, mapEquiv_symm_apply, map_mk', map_apply, map_id, map_bijective_iff_localizedModuleMap_bijective, IsLocalization.map_eq_toLinearMap_mapₐ, LocalizedModule.map_exact, map_injective_iff_localizedModuleMap_injective, ModuleCat.localizedModuleMap_hom_apply, map_exact, map_comp, IsLocalization.map_linearMap_eq_toLinearMap_mapₐ, map_surjective, map_iso_commute, map_LocalizedModules, Module.FinitePresentation.isLocalizedModule_map, LinearMap.toKerIsLocalized_apply_coe, map_lTensor, LinearMap.range_localizedMap_eq_localized₀_range
mk' 📖	CompOp	27 math math: Submodule.mem_localized', liftOfLE_mk', mk'_eq_zero', mk'_zero, mk'_add_mk', mk'_eq_mk'_iff, IsLocalization.mk'_eq_mk', IsLocalization.mk'_algebraMap_eq_mk', mk'_add, mk'_cancel', mk'_one, map_mk', mk'_cancel_right, mk'_neg, mk'_surjective, mk'_smul_mk', mk'_smul, mk_eq_mk', Submodule.mem_localized₀, mk'_sub, mk'_mul_mk', mk'_cancel, mk'_eq_zero, mk'_cancel_left, mk'_eq_iff, mk'_mul_mk'_of_map_mul, mk'_sub_mk'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_iff_exists 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	exists_of_eq smulCommClass_self IsScalarTower.left Module.End.isUnit_iff map_units LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul Submonoid.isScalarTower
eq_zero_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	mk'_eq_zero mk'_eq_zero'
exists_of_eq 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
ext 📖	—	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike LinearMap.comp RingHom.id RingHomCompTriple.ids	—	—	smulCommClass_self IsScalarTower.left RingHomCompTriple.ids lift_unique
fromLocalizedModule'_add 📖	mathematical	—	fromLocalizedModule' LocalizedModule OreLocalization.instAdd MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	LocalizedModule.induction_on₂ smulCommClass_self IsScalarTower.left map_units fromLocalizedModule'.congr_simp Module.End.algebraMap_isUnit_inv_apply_eq_iff smul_add map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass map_add SemilinearMapClass.toAddHomClass Module.End.algebraMap_isUnit_inv_apply_eq_iff' SemigroupAction.mul_smul Submonoid.coe_mul LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul Submonoid.isScalarTower mul_comm Submonoid.smul_def
fromLocalizedModule'_mk 📖	mathematical	—	fromLocalizedModule' DFunLike.coe Module.End CommSemiring.toSemiring LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Units.val Module.End.instMonoid Units Units.instInv IsUnit.unit RingHom Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike map_units LinearMap	—	—
fromLocalizedModule'_smul 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction fromLocalizedModule' LocalizedModule OreLocalization.instSMulOfIsScalarTower OreLocalization.oreSetComm CommSemiring.toCommMonoid DistribMulAction.toMulAction Algebra.toSMul Algebra.id IsScalarTower.left IsScalarTower.right	—	LocalizedModule.induction_on IsScalarTower.left IsScalarTower.right smulCommClass_self map_units LinearMap.map_smul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
fromLocalizedModule_mk 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LinearMap.instFunLike fromLocalizedModule Module.End Units.val Module.End.instMonoid Units Units.instInv IsUnit.unit RingHom Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommMonoid.toMonoid Algebra.toSMul Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike map_units	—	IsScalarTower.left IsScalarTower.right
injective_iff_isRegular 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike IsSMulRegular Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	eq_iff_exists
injective_of_map_eq 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	—	surj SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass Submonoid.smul_def LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul Submonoid.isScalarTower IsScalarTower.left mul_comm SemigroupAction.mul_smul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
injective_of_map_zero 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—	injective_of_map_eq sub_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
instIsTorsionFreeLocalizationLocalizedModuleOfIsDomain 📖	mathematical	—	Module.IsTorsionFree Localization CommRing.toCommMonoid LocalizedModule CommRing.toCommSemiring OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModule	—	isTorsionFree IsScalarTower.left IsScalarTower.right OreLocalization.instIsScalarTower_1 Localization.isLocalization localizedModuleIsLocalizedModule
instLiftOfLE 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder	IsLocalizedModule liftOfLE	—	map_units surj liftOfLE_apply mk'_surjective liftOfLE_mk' SMulCommClass.smul_comm smulCommClass_self one_smul
isRegular_of_smul_left_injective 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Commute.isRegular_iff Commute.all SemigroupAction.mul_smul
isScalarTower_module 📖	mathematical	—	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 module	—	LinearEquiv.isScalarTower IsScalarTower.left IsScalarTower.right LocalizedModule.instIsScalarTower RingHomInvPair.ids
isTorsionFree 📖	mathematical	—	Module.IsTorsionFree CommSemiring.toSemiring CommRing.toCommSemiring	—	isTorsionFree_of_forall_isRegular IsDomain.toIsCancelMulZero IsDomain.toNontrivial
isTorsionFree_of_forall_isRegular 📖	mathematical	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Module.IsTorsionFree CommSemiring.toSemiring CommRing.toCommSemiring	—	subsingleton_iff zero_smul IsLocalization.mk'_surjective mk'_surjective IsRegular.isSMulRegular One.instNonempty SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass SMulCommClass.smul_comm Submonoid.smulCommClass_left smulCommClass_self IsLocalization.isRegular_mk' mk'_smul_mk' SemigroupAction.mul_smul
is_universal 📖	mathematical	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	ExistsUnique LinearMap RingHom.id LinearMap.comp RingHomCompTriple.ids	—	smulCommClass_self IsScalarTower.left RingHomCompTriple.ids lift_comp lift_unique
iso_apply_mk 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id EquivLike.toFunLike LinearEquiv.instEquivLike iso Module.End LinearMap.instFunLike Units.val Module.End.instMonoid Units Units.instInv IsUnit.unit RingHom Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommMonoid.toMonoid Algebra.toSMul Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike map_units LinearMap	—	RingHomInvPair.ids IsScalarTower.left IsScalarTower.right
iso_localizedModule_eq_refl 📖	mathematical	—	iso LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LocalizedModule.mkLinearMap localizedModuleIsLocalizedModule LinearEquiv.refl	—	IsScalarTower.left IsScalarTower.right RingHomCompTriple.ids RingHomInvPair.ids localizedModuleIsLocalizedModule is_universal map_units LinearEquiv.eq_toLinearMap_symm_comp iso_symm_comp
iso_mk_one 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id EquivLike.toFunLike LinearEquiv.instEquivLike iso Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.one LinearMap LinearMap.instFunLike	—	RingHomInvPair.ids IsScalarTower.left IsScalarTower.right smulCommClass_self map_units map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsUnit.unit.congr_simp IsUnit.unit_one inv_one
iso_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm iso LinearMap LinearMap.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.one	—	DFunLike.congr_fun IsScalarTower.left IsScalarTower.right RingHomCompTriple.ids RingHomInvPair.ids iso_symm_comp
iso_symm_apply' 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike	LinearEquiv RingHomInvPair.ids LocalizedModule OreLocalization.instAddCommMonoidOreLocalization OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction IsScalarTower.right Algebra.id EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm iso	—	RingHomInvPair.ids IsScalarTower.left IsScalarTower.right surj iso_symm_apply_aux LocalizedModule.mk_eq eq_iff_exists Submonoid.smul_def LinearMap.map_smul SemigroupAction.mul_smul SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass mul_comm
iso_symm_apply_aux 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm iso Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul LinearMap LinearMap.instFunLike surj	—	LinearEquiv.injective IsScalarTower.left IsScalarTower.right RingHomInvPair.ids surj LinearEquiv.apply_symm_apply smulCommClass_self map_units
iso_symm_comp 📖	mathematical	—	LinearMap.comp LocalizedModule CommSemiring.toSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm iso LocalizedModule.mkLinearMap	—	LinearMap.ext IsScalarTower.left IsScalarTower.right RingHomCompTriple.ids RingHomInvPair.ids LinearMap.comp_apply LocalizedModule.mkLinearMap_apply LinearEquiv.coe_coe iso_symm_apply' one_smul
liftOfLE_apply 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder	DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike liftOfLE	—	lift_apply
liftOfLE_comp 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder	LinearMap.comp RingHom.id RingHomCompTriple.ids liftOfLE	—	lift_comp
liftOfLE_mk' 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder	DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike liftOfLE mk' SetLike.instMembership Submonoid.instSetLike	—	smulCommClass_self IsScalarTower.left Module.End.isUnit_iff map_units SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass mk'_cancel' liftOfLE.eq_1 lift_apply
lift_apply 📖	mathematical	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	LinearMap RingHom.id LinearMap.instFunLike lift	—	smulCommClass_self IsScalarTower.left LinearMap.congr_fun RingHomCompTriple.ids lift_comp
lift_comp 📖	mathematical	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	LinearMap.comp RingHom.id RingHomCompTriple.ids lift	—	smulCommClass_self IsScalarTower.left RingHomCompTriple.ids LinearMap.comp_assoc IsScalarTower.right RingHomInvPair.ids iso_symm_comp LocalizedModule.lift_comp
lift_comp_iso 📖	mathematical	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	LinearMap.comp LocalizedModule OreLocalization.instAddCommMonoidOreLocalization OreLocalization.oreSetComm OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.right RingHom.id RingHomCompTriple.ids lift LinearEquiv.toLinearMap RingHomInvPair.ids iso LocalizedModule.lift	—	smulCommClass_self IsScalarTower.left LinearMap.ext IsScalarTower.right RingHomCompTriple.ids RingHomInvPair.ids lift_iso
lift_iso 📖	mathematical	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	LinearMap RingHom.id LinearMap.instFunLike lift LinearEquiv RingHomInvPair.ids LocalizedModule OreLocalization.instAddCommMonoidOreLocalization OreLocalization.oreSetComm OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.right EquivLike.toFunLike LinearEquiv.instEquivLike iso LocalizedModule.lift	—	smulCommClass_self IsScalarTower.left RingHomInvPair.ids IsScalarTower.right LinearEquiv.symm_apply_apply
lift_unique 📖	mathematical	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike LinearMap.comp RingHom.id RingHomCompTriple.ids	lift	—	smulCommClass_self IsScalarTower.left RingHomCompTriple.ids IsScalarTower.right RingHomInvPair.ids LocalizedModule.lift_unique LinearMap.comp_assoc LinearMap.ext iso_mk_one LinearEquiv.comp_coe RingHomInvPair.triples₂ LinearEquiv.symm_trans_self LinearEquiv.refl_toLinearMap LinearMap.comp_id
linearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike linearEquiv LinearMap LinearMap.instFunLike	—	RingHomInvPair.ids iso_symm_apply iso_mk_one
linearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm linearEquiv LinearMap LinearMap.instFunLike	—	RingHomInvPair.ids iso_symm_apply iso_mk_one
linearMap_ext 📖	—	LinearMap.comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—	RingHomCompTriple.ids ExistsUnique.unique is_universal map_units
map_LocalizedModules 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommMonoid.toMonoid map LocalizedModule.mkLinearMap localizedModuleIsLocalizedModule	—	IsScalarTower.left IsScalarTower.right smulCommClass_self map_units localizedModuleIsLocalizedModule RingHomInvPair.ids LinearMap.comp.congr_simp iso_localizedModule_eq_refl LinearEquiv.refl_apply
map_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 map	—	lift_apply RingHomCompTriple.ids map_units
map_comp 📖	mathematical	—	LinearMap.comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike map	—	lift_comp RingHomCompTriple.ids map_units
map_comp' 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike map LinearMap.comp RingHomCompTriple.ids	—	LinearMap.ext smulCommClass_self RingHomCompTriple.ids mk'_surjective map_mk'
map_id 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike map LinearMap.id	—	LinearMap.ext smulCommClass_self mk'_surjective map_mk'
map_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	—	smulCommClass_self mk'_surjective map_mk' map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul Submonoid.isScalarTower IsScalarTower.left
map_iso_commute 📖	mathematical	—	LinearMap.comp LocalizedModule CommSemiring.toSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommMonoid.toMonoid LinearMap.instFunLike map LinearEquiv.toLinearMap RingHomInvPair.ids iso LocalizedModule.mkLinearMap localizedModuleIsLocalizedModule	—	LinearMap.ext IsScalarTower.left IsScalarTower.right RingHomCompTriple.ids smulCommClass_self RingHomInvPair.ids localizedModuleIsLocalizedModule LocalizedModule.induction_on Module.End.isUnit_iff map_units Module.algebraMap_end_apply LinearMap.CompatibleSMul.map_smul LinearMap.IsScalarTower.compatibleSMul OreLocalization.instIsScalarTower Submonoid.mk_smul LocalizedModule.mk_cancel iso_mk_one iso_symm_apply map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsUnit.unit.congr_simp IsUnit.unit_one inv_one LinearMap.comp.congr_simp iso_localizedModule_eq_refl
map_mk' 📖	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 mk'	—	smulCommClass_self map_units RingHomInvPair.ids IsScalarTower.left IsScalarTower.right iso_symm_apply' mk'_cancel'
map_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	—	smulCommClass_self mk'_surjective map_mk'
map_units 📖	mathematical	—	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	—
mem_ker_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	eq_zero_iff
mk'_add 📖	mathematical	—	mk' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	mk'_add_mk' smul_add mk'_cancel_left
mk'_add_mk' 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup mk' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Submonoid.mul	—	map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass
mk'_cancel 📖	mathematical	—	mk' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike	—	LocalizedModule.mk_cancel mk'_one smulCommClass_self IsScalarTower.left map_units IsScalarTower.right Module.End.algebraMap_isUnit_inv_apply_eq_iff SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass OneMemClass.coe_one one_smul
mk'_cancel' 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction mk' DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike	—	Submonoid.smul_def mk'_smul mk'_cancel
mk'_cancel_left 📖	mathematical	—	mk' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Submonoid.mul	—	LocalizedModule.mk_cancel_common_left
mk'_cancel_right 📖	mathematical	—	mk' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Submonoid.mul	—	LocalizedModule.mk_cancel_common_right
mk'_eq_iff 📖	mathematical	—	mk' DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Submonoid.smul_def mk'_smul mk'_cancel
mk'_eq_mk'_iff 📖	mathematical	—	mk' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	IsScalarTower.left IsScalarTower.right LocalizedModule.mk_eq
mk'_eq_zero 📖	mathematical	—	mk' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	mk'_eq_iff smul_zero
mk'_eq_zero' 📖	mathematical	—	mk' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	mk'_zero smul_zero one_smul
mk'_mul_mk' 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mk' NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule AlgHom.toLinearMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	mk'_mul_mk'_of_map_mul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
mk'_mul_mk'_of_map_mul 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	mk' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	Module.End.algebraMap_isUnit_inv_apply_eq_iff smul_smul_smul_comm IsScalarTower.left IsScalarTower.right Algebra.to_smulCommClass mk'_smul mk'_cancel
mk'_neg 📖	mathematical	—	mk' AddCommGroup.toAddCommMonoid SubtractionCommMonoid.toAddCommMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	LocalizedModule.mk_neg map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
mk'_one 📖	mathematical	—	mk' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.one DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike	—	smulCommClass_self IsScalarTower.left map_units IsScalarTower.right Module.End.algebraMap_isUnit_inv_apply_eq_iff Submonoid.coe_one one_smul
mk'_smul 📖	mathematical	—	mk' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	IsScalarTower.left IsScalarTower.right map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
mk'_smul_mk' 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction IsLocalization.mk' mk' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	smul_injective SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass SemigroupAction.mul_smul SMulCommClass.smul_comm Submonoid.smulCommClass_left IsScalarTower.to_smulCommClass mk'_cancel' Submonoid.smul_def map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass smul_assoc IsLocalization.smul_mk'_self algebraMap_smul
mk'_sub 📖	mathematical	—	mk' AddCommGroup.toAddCommMonoid SubtractionCommMonoid.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SubtractionMonoid.toSubNegMonoid SubtractionCommMonoid.toSubtractionMonoid	—	sub_eq_add_neg mk'_add mk'_neg
mk'_sub_mk' 📖	mathematical	—	SubNegMonoid.toSub SubtractionMonoid.toSubNegMonoid SubtractionCommMonoid.toSubtractionMonoid mk' AddCommGroup.toAddCommMonoid SubtractionCommMonoid.toAddCommMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Submonoid.mul	—	sub_eq_add_neg mk'_neg mk'_add_mk' smul_neg
mk'_surjective 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike mk'	—	surj mk'_eq_iff
mk'_zero 📖	mathematical	—	mk' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	zero_smul mk'_smul
mkOfAlgebra 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.smul Algebra.toSMul AlgHom AlgHom.funLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	IsLocalizedModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule AlgHom.toLinearMap	—	IsUnit.mul_left_cancel Algebra.smul_def MulZeroClass.mul_zero map_smul SemilinearMapClass.toMulActionSemiHomClass AlgHomClass.linearMapClass AlgHom.algHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.congr_arg smulCommClass_self IsScalarTower.left Module.End.isUnit_iff Module.algebraMap_end_apply mul_assoc IsUnit.mul_val_inv one_mul sub_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass smul_sub
mk_eq_mk' 📖	mathematical	—	mk' LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LocalizedModule.mkLinearMap localizedModuleIsLocalizedModule	—	IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule mk'_eq_iff Submonoid.smul_def LocalizedModule.mk_cancel LocalizedModule.mkLinearMap_apply
of_exists_mul_mem 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder SetLike.instMembership Submonoid.instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	IsLocalizedModule	—	smulCommClass_self IsScalarTower.left map_units Commute.isUnit_mul_iff Algebra.commute_algebraMap_left map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass surj exists_of_eq
of_linearEquiv 📖	mathematical	—	IsLocalizedModule LinearMap.comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids	—	RingHomInvPair.ids RingHomCompTriple.ids smulCommClass_self IsScalarTower.left LinearMap.ext map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearEquiv.apply_symm_apply Module.End.isUnit_iff LinearMap.coe_comp LinearEquiv.coe_coe EquivLike.comp_bijective EquivLike.bijective_comp map_units surj LinearEquiv.congr_arg Submonoid.smul_def exists_of_eq EquivLike.toEmbeddingLike
of_linearEquiv_right 📖	mathematical	—	IsLocalizedModule LinearMap.comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids	—	RingHomInvPair.ids RingHomCompTriple.ids map_units surj LinearEquiv.apply_symm_apply exists_of_eq map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearEquiv.symm_apply_apply
of_restrictScalars 📖	mathematical	—	IsLocalizedModule Algebra.algebraMapSubmonoid CommSemiring.toSemiring	—	LinearMap.IsScalarTower.compatibleSMul smulCommClass_self IsScalarTower.left map_units IsScalarTower.to_smulCommClass' LinearMap.instIsScalarTower surj algebraMap_smul exists_of_eq
smul_inj 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	smul_injective
smul_injective 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Function.Bijective.injective smulCommClass_self IsScalarTower.left Module.End.isUnit_iff map_units
subsingleton_iff 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	subsingleton_iff_ker_eq_top instIsConcreteLE mem_ker_iff
subsingleton_iff_ker_eq_top 📖	mathematical	—	LinearMap.ker CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Top.top Submodule Submodule.instTop	—	top_le_iff mk'_surjective Submodule.mem_top
subsingleton_of_subsingleton 📖	—	—	—	—	subsingleton_iff SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass smul_zero
surj 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike	—	—
surj' 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike	—	surj

IsLocalizedModule.fromLocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bij 📖	mathematical	—	Function.Bijective LocalizedModule DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LinearMap.instFunLike IsLocalizedModule.fromLocalizedModule	—	IsScalarTower.left IsScalarTower.right surj
inj 📖	mathematical	—	LocalizedModule DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LinearMap.instFunLike IsLocalizedModule.fromLocalizedModule	—	IsScalarTower.left IsScalarTower.right LocalizedModule.induction_on LocalizedModule.mk_eq IsLocalizedModule.eq_iff_exists Submonoid.smul_def LinearMap.map_smul smulCommClass_self IsLocalizedModule.map_units Module.End.algebraMap_isUnit_inv_apply_eq_iff' map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Module.End.algebraMap_isUnit_inv_apply_eq_iff
surj 📖	mathematical	—	LocalizedModule DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LinearMap.instFunLike IsLocalizedModule.fromLocalizedModule	—	IsScalarTower.left IsScalarTower.right IsLocalizedModule.surj smulCommClass_self IsLocalizedModule.map_units Module.End.algebraMap_isUnit_inv_apply_eq_iff Submonoid.smul_def

LocalizedModule

Definitions

Name	Category	Theorems
algebra' 📖	CompOp	—
algebraOfIsLocalization 📖	CompOp	2 math math: algebraMap_mk, algebraMap_mk'
divBy 📖	CompOp	3 math math: divBy_apply, divBy_mul_by, mul_by_divBy
instCommRing 📖	CompOp	1 math math: AlgebraicGeometry.structureSheafInType.mul_apply
instCommSemiring 📖	CompOp	—
instMonoid 📖	CompOp	2 math math: mk_mul_mk, mk_mul_mk'
instRing 📖	CompOp	—
instSemiring 📖	CompOp	4 math math: smul'_mul, algebraMap_mk, mul_smul', algebraMap_mk'
lift' 📖	CompOp	3 math math: lift'_smul, lift'_mk, lift'_add
liftOfLE 📖	CompOp	—
liftOn 📖	CompOp	2 math math: liftOn_mk, divBy_apply
liftOn₂ 📖	CompOp	1 math math: liftOn₂_mk
mk 📖	CompOp	—
mkLinearMap 📖	CompOp	15 math math: mem_ker_mkLinearMap_iff, Module.FinitePresentation.linearEquivMap_symm_apply, IsLocalizedModule.iso_symm_comp, subsingleton_iff_ker_eq_top, Module.FinitePresentation.linearEquivMap_apply, localizedModuleIsLocalizedModule, lift_comp, Module.FinitePresentation.linearEquivMapExtendScalars_apply, map_exact, IsLocalizedModule.mk_eq_mk', IsLocalizedModule.iso_localizedModule_eq_refl, IsLocalizedModule.map_iso_commute, IsLocalizedModule.map_LocalizedModules, mkLinearMap_apply, Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply
moduleOfIsLocalization 📖	CompOp	—
mul 📖	CompOp	—
numeratorRingHom 📖	CompOp	—
r 📖	MathDef	2 math math: r.isEquiv, oreEqv_eq_r
smulOfIsLocalization 📖	CompOp	5 math math: smul'_mul, smul_def, instIsScalarTower, mk'_smul_mk, mul_smul'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_mk 📖	mathematical	—	DFunLike.coe RingHom Localization CommSemiring.toCommMonoid LocalizedModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule CommSemiring.toSemiring OreLocalization.instCommSemiring OreLocalization.oreSetComm instSemiring RingHom.instFunLike algebraMap algebraOfIsLocalization OreLocalization.instAlgebra Algebra.id Localization.isLocalization	—	Localization.isLocalization Localization.mk_eq_mk' algebraMap_mk'
algebraMap_mk' 📖	mathematical	—	DFunLike.coe RingHom LocalizedModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule CommSemiring.toSemiring instSemiring RingHom.instFunLike algebraMap algebraOfIsLocalization IsLocalization.mk'	—	Algebra.algebraMap_eq_smul_one mul_one
divBy_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LinearMap.instFunLike divBy liftOn Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	IsScalarTower.left IsScalarTower.right
divBy_mul_by 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LinearMap.instFunLike divBy Module.End RingHom Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra OreLocalization.instSMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.to_smulCommClass Algebra.toSMul OreLocalization.instIsScalarTower Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	induction_on IsScalarTower.left IsScalarTower.right OreLocalization.instSMulCommClass Algebra.to_smulCommClass OreLocalization.instIsScalarTower Module.algebraMap_end_apply divBy_apply Submonoid.smul_def mk_cancel_common_right
eq_zero_of_smul_eq_zero 📖	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike LocalizedModule OreLocalization.instSMulOfIsScalarTower MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Algebra.toSMul Algebra.id IsScalarTower.left IsScalarTower.right OreLocalization.instZero	—	—	IsScalarTower.left IsScalarTower.right smul_eq_iff_of_mem smul_zero
induction_on 📖	—	—	—	—	—
induction_on₂ 📖	—	—	—	—	—
instIsScalarTower 📖	mathematical	—	IsScalarTower LocalizedModule Algebra.toSMul CommSemiring.toSemiring smulOfIsLocalization OreLocalization.instSMulOfIsScalarTower MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Algebra.id IsScalarTower.left IsScalarTower.right	—	IsScalarTower.left IsScalarTower.right induction_on IsLocalization.mk'_sec IsLocalization.smul_mk' SemigroupAction.mul_smul
instSubsingleton 📖	mathematical	—	LocalizedModule CommRing.toCommSemiring	—	IsLocalizedModule.subsingleton_iff IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule Submonoid.one_mem
lift'_add 📖	mathematical	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	lift' LocalizedModule OreLocalization.instAdd OreLocalization.oreSetComm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self IsScalarTower.left induction_on₂ map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Module.End.algebraMap_isUnit_inv_apply_eq_iff smul_add map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul Submonoid.isScalarTower SemigroupAction.mul_smul Submonoid.smul_def mul_comm
lift'_mk 📖	mathematical	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	lift' LinearMap.instFunLike RingHom.id Units.val Units Units.instInv IsUnit.unit LinearMap	—	smulCommClass_self IsScalarTower.left
lift'_smul 📖	mathematical	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul lift' LocalizedModule OreLocalization.instSMulOfIsScalarTower OreLocalization.oreSetComm IsScalarTower.right	—	smulCommClass_self IsScalarTower.left induction_on IsScalarTower.right map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.map_smul
liftOn_mk 📖	mathematical	—	liftOn Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike	—	—
liftOn₂_mk 📖	mathematical	—	liftOn₂ Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike	—	—
lift_comp 📖	mathematical	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	LinearMap.comp LocalizedModule OreLocalization.instAddCommMonoidOreLocalization OreLocalization.oreSetComm OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.right RingHom.id RingHomCompTriple.ids lift mkLinearMap	—	smulCommClass_self IsScalarTower.left LinearMap.ext IsScalarTower.right RingHomCompTriple.ids map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsUnit.unit.congr_simp IsUnit.unit_one inv_one
lift_mk 📖	mathematical	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	LinearMap RingHom.id LocalizedModule OreLocalization.instAddCommMonoidOreLocalization OreLocalization.oreSetComm OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.right LinearMap.instFunLike lift Units.val Units Units.instInv IsUnit.unit	—	smulCommClass_self IsScalarTower.left IsScalarTower.right
lift_mk_one 📖	mathematical	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	LinearMap RingHom.id LocalizedModule OreLocalization.instAddCommMonoidOreLocalization OreLocalization.oreSetComm OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.right LinearMap.instFunLike lift Submonoid.one	—	smulCommClass_self IsScalarTower.left IsScalarTower.right map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsUnit.unit.congr_simp IsUnit.unit_one inv_one
lift_unique 📖	mathematical	IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike LinearMap.comp LocalizedModule OreLocalization.instAddCommMonoidOreLocalization OreLocalization.oreSetComm OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.right RingHom.id RingHomCompTriple.ids mkLinearMap	lift	—	smulCommClass_self IsScalarTower.left IsScalarTower.right RingHomCompTriple.ids LinearMap.ext induction_on Module.End.algebraMap_isUnit_inv_apply_eq_iff LinearMap.coe_comp mkLinearMap_apply LinearMap.map_smul mk_eq one_smul
mem_ker_mkLinearMap_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike LinearMap.ker LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id RingHom.id Semiring.toNonAssocSemiring mkLinearMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	IsLocalizedModule.mem_ker_iff IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule
mk'_smul_mk 📖	mathematical	—	LocalizedModule smulOfIsLocalization IsLocalization.mk' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	smul_def mk_eq IsLocalization.eq IsLocalization.mk'_sec mul_comm mul_assoc
mkLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LinearMap.instFunLike mkLinearMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.one	—	IsScalarTower.left IsScalarTower.right
mk_add_mk 📖	mathematical	—	LocalizedModule OreLocalization.instAdd MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Submonoid.mul	—	SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass OreLocalization.oreDiv_add_oreDiv mul_comm
mk_cancel 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Submonoid.one	—	mk_eq one_smul
mk_cancel_common_left 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Submonoid.mul	—	mk_eq SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass one_smul SemigroupAction.mul_smul SMulCommClass.smul_comm Submonoid.smulCommClass_left Submonoid.smulCommClass_right smulCommClass_self
mk_cancel_common_right 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Submonoid.mul	—	mk_eq SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass one_smul SemigroupAction.mul_smul
mk_eq 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	OreLocalization.oreDiv_eq_iff oreEqv_eq_r
mk_mul_mk 📖	mathematical	—	LocalizedModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	mk_mul_mk' SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass mul_comm
mk_mul_mk' 📖	mathematical	—	LocalizedModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	—
mk_neg 📖	mathematical	—	AddCommGroup.toAddCommMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LocalizedModule OreLocalization.instNegOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommGroup.toAddGroup Module.toDistribMulAction	—	OreLocalization.neg_def
mk_smul_mk 📖	mathematical	—	Localization CommSemiring.toCommMonoid LocalizedModule OreLocalization.instSMul CommMonoid.toMonoid OreLocalization.oreSetComm DistribMulAction.toMulAction MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	OreLocalization.oreDiv_smul_char mul_comm SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass
mul_by_divBy 📖	mathematical	—	DFunLike.coe Module.End LocalizedModule CommSemiring.toSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring RingHom Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra OreLocalization.instSMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.to_smulCommClass Algebra.toSMul OreLocalization.instIsScalarTower Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike LinearMap divBy	—	induction_on IsScalarTower.left IsScalarTower.right OreLocalization.instSMulCommClass Algebra.to_smulCommClass OreLocalization.instIsScalarTower divBy_apply Module.algebraMap_end_apply Submonoid.smul_def mk_cancel_common_right
mul_smul' 📖	mathematical	—	LocalizedModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instSemiring smulOfIsLocalization	—	induction_on₂ smul_def SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass mul_left_comm mul_smul_comm Algebra.to_smulCommClass
oreEqv_eq_r 📖	mathematical	—	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike OreLocalization.oreEqv OreLocalization.oreSetComm CommSemiring.toCommMonoid DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction r	—	smul_smul mul_comm SemigroupAction.mul_smul Submonoid.smul_def SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass Submonoid.coe_mul mul_assoc
smul'_mk 📖	mathematical	—	LocalizedModule OreLocalization.instSMulOfIsScalarTower MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Algebra.toSMul Algebra.id IsScalarTower.left IsScalarTower.right	—	IsScalarTower.left IsScalarTower.right OreLocalization.smul_oreDiv mul_one
smul'_mul 📖	mathematical	—	LocalizedModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instSemiring smulOfIsLocalization	—	induction_on₂ smul_def SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass mul_assoc smul_mul_assoc IsScalarTower.right
smul_def 📖	mathematical	—	LocalizedModule smulOfIsLocalization SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike IsLocalization.sec Submonoid.mul	—	—
smul_eq_iff_of_mem 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike	LocalizedModule OreLocalization.instSMulOfIsScalarTower MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Algebra.toSMul Algebra.id IsScalarTower.left IsScalarTower.right Localization OreLocalization.instSMul CommMonoid.toMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Monoid.toMulOneClass	—	induction_on IsScalarTower.left IsScalarTower.right one_smul mk_eq SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass SemigroupAction.mul_smul Submonoid.mk_smul SMulCommClass.smul_comm Submonoid.smulCommClass_right smulCommClass_self mul_comm Submonoid.smul_def
subsingleton 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	LocalizedModule	—	induction_on₂ mk_eq zero_smul
subsingleton_iff 📖	mathematical	—	LocalizedModule CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	IsLocalizedModule.subsingleton_iff IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule
subsingleton_iff_ker_eq_top 📖	mathematical	—	LocalizedModule CommRing.toCommSemiring LinearMap.ker CommSemiring.toSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id RingHom.id Semiring.toNonAssocSemiring mkLinearMap Top.top Submodule Submodule.instTop	—	IsLocalizedModule.subsingleton_iff_ker_eq_top IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule
zero_mk 📖	mathematical	—	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LocalizedModule OreLocalization.instZero MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid DistribMulAction.toMulAction Module.toDistribMulAction	—	OreLocalization.zero_oreDiv

LocalizedModule.r

Definitions

Name	Category	Theorems
setoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isEquiv 📖	mathematical	—	IsEquiv Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike LocalizedModule.r	—	one_smul SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass mul_comm mul_left_comm

(root)

Definitions

Name	Category	Theorems
IsLocalizedModule 📖	CompData	43 math math: IsLocalizedModule.instLiftOfLE, IsLocalization.instIsLocalizedModuleTensorProductMap, KaehlerDifferential.isLocalizedModule_of_isLocalizedModule, isLocalizedModule_iff_isBaseChange, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ, LinearMap.toKerLocalized_isLocalizedModule, IsLocalization.tensorProduct_isLocalizedModule, Submodule.isLocalizedModule, KaehlerDifferential.isLocalizedModule_map, IsLocalizedModule.of_restrictScalars, ModuleCat.localizedModule_isLocalizedModule, isLocalizedModule_iff, instIsLocalizedModuleFinsuppLinearMap, isLocalizedModule_iff_isLocalization, instIsLocalizedModuleLinearMapOfIsLocalization, Algebra.IsAlgebraic.instIsLocalizedModuleNonZeroDivisorsToLinearMapToAlgHom, IsLocalizedModule.exists_isLocalizedModule_powers_of_finitePresentation, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, IsLocalizedModule.toLocalizedQuotient', localizedModuleIsLocalizedModule, IsLocalizedModule.rTensor, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient, instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid, IsLocalizedModule.of_exists_mul_mem, IsLocalizedModule.prodMap, Algebra.idealMap_isLocalizedModule, KaehlerDifferential.isLocalizedModule, isLocalizedModule_id, isLocalizedModule_iff_isLocalization', AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, IsLocalizedModule.mkOfAlgebra, Algebra.H1Cotangent.isLocalizedModule, AlgHom.toKerIsLocalization_isLocalizedModule, Module.FinitePresentation.isLocalizedModule_mapExtendScalars, IsLocalizedModule.of_linearEquiv, NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation, RingHom.toKerIsLocalization_isLocalizedModule, Module.FinitePresentation.isLocalizedModule_map, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen, IsLocalizedModule.of_linearEquiv_right, Submodule.instIsLocalizedModuleSubtypeMemLocalized₀ToLocalized₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalizedModule_id 📖	mathematical	—	IsLocalizedModule LinearMap.id CommSemiring.toSemiring	—	smulCommClass_self IsScalarTower.left IsScalarTower.to_smulCommClass' AlgHom.commutes IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass IsLocalization.map_units one_smul
isLocalizedModule_iff 📖	mathematical	—	IsLocalizedModule IsUnit Module.End CommSemiring.toSemiring Module.End.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul LinearMap RingHom.id LinearMap.instFunLike	—	smulCommClass_self IsScalarTower.left
localizedModuleIsLocalizedModule 📖	mathematical	—	IsLocalizedModule LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LocalizedModule.mkLinearMap	—	IsScalarTower.left IsScalarTower.right smulCommClass_self OreLocalization.instSMulCommClass Algebra.to_smulCommClass OreLocalization.instIsScalarTower DFunLike.ext LocalizedModule.mul_by_divBy LocalizedModule.divBy_mul_by LocalizedModule.induction_on Submonoid.smul_def LocalizedModule.mkLinearMap_apply LocalizedModule.mk_cancel one_smul LocalizedModule.mk_eq

---

← Back to Index