Documentation Verification Report

BaseChange

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

Statistics

Metric	Count
Definitions `tensorEquiv`, `tensorRightEquiv`, `algebraLid`, `algebraTensorEquiv`, `moduleLid`, `moduleTensorEquiv`, `equivTensorProduct`	7
Theorems `isLocalization_iff_isPushout`, `isPushout_of_isLocalization`, `tensor`, `tensorRight`, `bijective_linearMap_mul'`, `instCompatibleSMulLocalizationOfIsScalarTower_1`, `instIsLocalizedModuleTensorProductMap`, `mk'_tmul`, `tensor`, `tensorProduct_compatibleSMul`, `tensorProduct_isLocalizedModule`, `tensorProduct_tensorProduct`, `tensorRight`, `tmul_mk'`, `isBaseChange`, `map_lTensor`, `map_linearCombination`, `rTensor`, `equivTensorProduct_apply_mk`, `equivTensorProduct_symm_apply_tmul`, `equivTensorProduct_symm_apply_tmul_one`, `instIsLocalizedModuleFinsuppLinearMap`, `isLocalizedModule_iff_isBaseChange`	23
Total	30

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalization_iff_isPushout` 📖	mathematical	—	`IsLocalization` `algebraMapSubmonoid` `CommSemiring.toSemiring` `IsPushout`	—	`IsPushout.comm` `isPushout_iff` `isLocalizedModule_iff_isLocalization` `isLocalizedModule_iff_isBaseChange`
`isPushout_of_isLocalization` 📖	mathematical	—	`IsPushout`	—	`isLocalization_iff_isPushout`

IsLocalization

Definitions

Name	Category	Theorems
`algebraLid` 📖	CompOp	—
`algebraTensorEquiv` 📖	CompOp	—
`moduleLid` 📖	CompOp	—
`moduleTensorEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_linearMap_mul'` 📖	mathematical	—	`Function.Bijective` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.mul'` `Algebra.to_smulCommClass` `IsScalarTower.right`	—	`tensorProduct_compatibleSMul` `IsScalarTower.right` `AlgEquiv.bijective` `Algebra.to_smulCommClass`
`instCompatibleSMulLocalizationOfIsScalarTower_1` 📖	mathematical	—	`TensorProduct.CompatibleSMul` `Localization` `CommSemiring.toCommMonoid` `OreLocalization.instMonoid` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `Module.toDistribMulAction` `OreLocalization.instSemiring` `CommSemiring.toSemiring`	—	`IsScalarTower.right` `tensorProduct_compatibleSMul` `Localization.isLocalization`
`instIsLocalizedModuleTensorProductMap` 📖	mathematical	—	`IsLocalizedModule` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.map` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`RingHomInvPair.ids` `IsScalarTower.right` `TensorProduct.smulCommClass_left` `smulCommClass_self` `tensorProduct_isLocalizedModule` `Localization.isLocalization` `RingHomCompTriple.ids` `Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass'` `LinearMap.IsScalarTower.compatibleSMul` `TensorProduct.isScalarTower_left` `TensorProduct.isScalarTower` `TensorProduct.CompatibleSMul.isScalarTower` `instCompatibleSMulLocalizationOfIsScalarTower_1` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `IsLocalizedModule.linearEquiv_apply` `IsLocalizedModule.of_linearEquiv`
`mk'_tmul` 📖	mathematical	—	`TensorProduct.tmul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `mk'` `Algebra.algebraMapSubmonoid` `TensorProduct` `Algebra.TensorProduct.instCommSemiring` `Algebra.TensorProduct.rightAlgebra` `tensorRight` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Algebra.mem_algebraMapSubmonoid_of_mem`	—	`tensorRight` `Algebra.mem_algebraMapSubmonoid_of_mem` `AlgHom.commutes` `mk'_spec` `mul_one` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Algebra.to_smulCommClass` `IsScalarTower.right` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `one_mul`
`tensor` 📖	mathematical	—	`IsLocalization` `Algebra.algebraMapSubmonoid` `CommSemiring.toSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instCommSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	—	`Algebra.to_smulCommClass` `Algebra.TensorProduct.right_isScalarTower` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `Algebra.isLocalization_iff_isPushout` `TensorProduct.isPushout`
`tensorProduct_compatibleSMul` 📖	mathematical	—	`TensorProduct.CompatibleSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction`	—	`exists_mk'_eq` `IsScalarTower.to_smulCommClass` `IsUnit.smul_left_cancel` `map_units` `algebraMap_smul` `TensorProduct.isScalarTower_left` `TensorProduct.smul_tmul` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left` `smul_mk'_self`
`tensorProduct_isLocalizedModule` 📖	mathematical	—	`IsLocalizedModule` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `DFunLike.coe` `LinearMap` `RingHom.id` `LinearMap.addCommMonoid` `LinearMap.module` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `LinearMap.instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`TensorProduct.smulCommClass_left` `smulCommClass_self` `Algebra.to_smulCommClass` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `isLocalizedModule_iff_isBaseChange` `TensorProduct.isBaseChange`
`tensorProduct_tensorProduct` 📖	mathematical	`RingHom.comp` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRing.toCommSemiring` `Algebra.TensorProduct.instCommSemiring` `Algebra.TensorProduct.instSemiring` `algebraMap` `AlgHom.toRingHom` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight`	`IsLocalization` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instCommSemiring` `Algebra.algebraMapSubmonoid` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRing.toCommSemiring`	—	`Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `Algebra.isLocalization_iff_isPushout` `Algebra.IsPushout.symm` `Algebra.IsPushout.tensorProduct_tensorProduct`
`tensorRight` 📖	mathematical	—	`IsLocalization` `Algebra.algebraMapSubmonoid` `CommSemiring.toSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instCommSemiring` `Algebra.TensorProduct.rightAlgebra`	—	`Algebra.to_smulCommClass` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `Algebra.TensorProduct.right_isScalarTower` `Algebra.isLocalization_iff_isPushout` `TensorProduct.isPushout'`
`tmul_mk'` 📖	mathematical	—	`TensorProduct.tmul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `mk'` `Algebra.algebraMapSubmonoid` `TensorProduct` `Algebra.TensorProduct.instCommSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `tensor` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Algebra.mem_algebraMapSubmonoid_of_mem`	—	`Algebra.to_smulCommClass` `tensor` `Algebra.mem_algebraMapSubmonoid_of_mem` `eq_mk'_iff_mul_eq` `Algebra.TensorProduct.algebraMap_apply` `Algebra.algebraMap_self` `RingHomCompTriple.comp_apply` `RingHomCompTriple.right_ids` `Algebra.TensorProduct.tmul_one_eq_one_tmul` `IsScalarTower.right` `Algebra.TensorProduct.tmul_mul_tmul` `mul_one` `mul_comm` `mk'_spec'` `RingHom.id_apply` `Algebra.smul_def` `TensorProduct.smul_tmul` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left`

IsLocalization.Away

Definitions

Name	Category	Theorems
`tensorEquiv` 📖	CompOp	—
`tensorRightEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tensor` 📖	mathematical	—	`IsLocalization.Away` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instCommSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	—	`Algebra.to_smulCommClass` `IsLocalization.tensor`
`tensorRight` 📖	mathematical	—	`IsLocalization.Away` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instCommSemiring` `Algebra.TensorProduct.rightAlgebra`	—	`IsLocalization.tensorRight`

IsLocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBaseChange` 📖	mathematical	—	`IsBaseChange`	—	`IsBaseChange.of_lift_unique` `RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `is_universal` `smulCommClass_self` `IsScalarTower.left` `IsScalarTower.to_smulCommClass'` `AlgHom.commutes` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsLocalization.map_units`
`map_lTensor` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `map` `IsScalarTower.to_smulCommClass'` `TensorProduct.instModule` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `TensorProduct.AlgebraTensorModule.rTensor` `rTensor` `TensorProduct.AlgebraTensorModule.lTensor`	—	`linearMap_ext` `IsScalarTower.to_smulCommClass` `IsScalarTower.to_smulCommClass'` `TensorProduct.smulCommClass_left` `rTensor` `smulCommClass_self` `RingHomCompTriple.ids` `map_comp` `TensorProduct.AlgebraTensorModule.curry_injective` `TensorProduct.isScalarTower_left` `LinearMap.ext` `LinearMap.IsScalarTower.compatibleSMul` `LinearMap.rTensor_comp_lTensor` `LinearMap.lTensor_comp_rTensor`
`map_linearCombination` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `Finsupp.module` `Semiring.toModule` `Algebra.toModule` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `map` `Finsupp.mapRange.linearMap` `Algebra.linearMap` `instIsLocalizedModuleFinsuppLinearMap` `instIsLocalizedModuleLinearMapOfIsLocalization` `Finsupp.linearCombination` `LinearMap.restrictScalars` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `LinearMap.CompatibleSMul.finsupp_dom` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearMap.IsScalarTower.compatibleSMul'` `SMulZeroClass.toSMul`	—	`linearMap_ext` `instIsLocalizedModuleFinsuppLinearMap` `instIsLocalizedModuleLinearMapOfIsLocalization` `smulCommClass_self` `LinearMap.CompatibleSMul.finsupp_dom` `LinearMap.IsScalarTower.compatibleSMul'` `Finsupp.lhom_ext'` `RingHomCompTriple.ids` `LinearMap.ext_ring` `LinearMap.comp.congr_simp` `map_comp` `Finsupp.linearCombination_single` `one_smul` `LinearMap.map_zero` `Finsupp.mapRange_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`rTensor` 📖	mathematical	—	`IsLocalizedModule` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `CommSemiring.toSemiring` `IsScalarTower.to_smulCommClass` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `LinearMap.module` `IsScalarTower.to_smulCommClass'` `TensorProduct.instModule` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `LinearMap.instFunLike` `TensorProduct.AlgebraTensorModule.rTensor`	—	`IsScalarTower.to_smulCommClass` `IsScalarTower.to_smulCommClass'` `TensorProduct.smulCommClass_left` `RingHomInvPair.ids` `IsScalarTower.left` `IsScalarTower.right` `IsScalarTower.of_algebraMap_smul` `IsScalarTower.algebraMap_apply` `OreLocalization.instIsScalarTower` `algebraMap_smul` `LinearEquiv.isScalarTower` `OreLocalization.instIsScalarTower_1` `TensorProduct.isScalarTower_left` `isLocalizedModule_iff_isBaseChange` `Localization.isLocalization` `isBaseChange_tensorProduct_map`

LocalizedModule

Definitions

Name	Category	Theorems
`equivTensorProduct` 📖	CompOp	3 math math: `equivTensorProduct_symm_apply_tmul_one`, `equivTensorProduct_apply_mk`, `equivTensorProduct_symm_apply_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivTensorProduct_apply_mk` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Localization` `CommSemiring.toCommMonoid` `OreLocalization.instSemiring` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LocalizedModule` `TensorProduct` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `Semiring.toModule` `OreLocalization.instModuleOfIsScalarTower` `IsScalarTower.right` `Algebra.id` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `TensorProduct.addCommMonoid` `OreLocalization.instModule` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `OreLocalization.instAlgebra` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `equivTensorProduct` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`LinearEquiv.injective` `IsScalarTower.right` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `LinearEquiv.symm_apply_apply` `IsScalarTower.left` `equivTensorProduct_symm_apply_tmul` `one_smul`
`equivTensorProduct_symm_apply_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Localization` `CommSemiring.toCommMonoid` `OreLocalization.instSemiring` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `Semiring.toModule` `OreLocalization.instModuleOfIsScalarTower` `IsScalarTower.right` `Algebra.id` `LocalizedModule` `TensorProduct.addCommMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `TensorProduct.leftModule` `OreLocalization.instModule` `Algebra.to_smulCommClass` `OreLocalization.instAlgebra` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `equivTensorProduct` `TensorProduct.tmul` `OreLocalization.instSMulOfIsScalarTower` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Algebra.toSMul` `IsScalarTower.left`	—	`RingHomInvPair.ids` `IsScalarTower.right` `Algebra.to_smulCommClass` `IsScalarTower.left` `mul_one`
`equivTensorProduct_symm_apply_tmul_one` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Localization` `CommSemiring.toCommMonoid` `OreLocalization.instSemiring` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `Semiring.toModule` `OreLocalization.instModuleOfIsScalarTower` `IsScalarTower.right` `Algebra.id` `LocalizedModule` `TensorProduct.addCommMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `TensorProduct.leftModule` `OreLocalization.instModule` `Algebra.to_smulCommClass` `OreLocalization.instAlgebra` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `equivTensorProduct` `TensorProduct.tmul` `OreLocalization.instOne` `Monoid.toMulAction` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.one`	—	`RingHomInvPair.ids` `IsScalarTower.right` `Algebra.to_smulCommClass` `IsScalarTower.left` `equivTensorProduct_symm_apply_tmul` `one_smul`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLocalizedModuleFinsuppLinearMap` 📖	mathematical	—	`IsLocalizedModule` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `CommSemiring.toSemiring` `Finsupp.mapRange.linearMap` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`RingHomInvPair.ids` `IsScalarTower.right` `IsScalarTower.left` `RingHomCompTriple.ids` `Algebra.to_smulCommClass` `LinearMap.IsScalarTower.compatibleSMul` `TensorProduct.isScalarTower_left` `OreLocalization.instIsScalarTower_1` `IsScalarTower.to_smulCommClass` `OreLocalization.instIsScalarTower` `isLocalizedModule_iff_isBaseChange` `Localization.isLocalization` `TensorProduct.smulCommClass_left` `smulCommClass_self` `Finsupp.lhom_ext'` `LinearMap.ext` `LinearEquiv.injective` `Finsupp.ext` `LocalizedModule.equivTensorProduct_symm_apply_tmul_one` `IsLocalizedModule.iso_mk_one` `TensorProduct.tmul_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearMap.comp.congr_simp` `LinearEquiv.trans.congr_simp` `Finsupp.mapRange.linearEquiv_symm` `Finsupp.mapRange_single` `LinearMap.map_zero` `LinearEquiv.map_zero` `LinearEquiv.apply_symm_apply` `Finsupp.single_apply` `TensorProduct.finsuppRight_tmul_single` `TensorProduct.isBaseChange` `LinearEquiv.comp_symm_assoc` `IsLocalizedModule.of_linearEquiv`
`isLocalizedModule_iff_isBaseChange` 📖	mathematical	—	`IsLocalizedModule` `IsBaseChange`	—	`IsLocalizedModule.isBaseChange` `IsScalarTower.left` `IsScalarTower.right` `LocalizedModule.instIsScalarTower` `localizedModuleIsLocalizedModule` `RingHomInvPair.ids` `LinearMap.IsScalarTower.compatibleSMul` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `LinearMap.ext` `LinearMap.coe_comp` `LinearEquiv.coe_coe` `LinearEquiv.restrictScalars_apply` `LinearEquiv.trans_apply` `IsBaseChange.equiv_symm_apply` `IsBaseChange.equiv_tmul` `one_smul` `IsLocalizedModule.of_linearEquiv`

---

← Back to Index