Documentation Verification Report

IsTensorProduct

📁 Source: Mathlib/RingTheory/IsTensorProduct.lean

Statistics

Metric	Count
Definitions `IsPushout`, `cancelBaseChange`, `cancelBaseChangeAlg`, `cancelBaseChangeAux`, `equiv`, `pushoutDesc`, `IsBaseChange`, `equiv`, `tensorEquiv`, `IsTensorProduct`, `assoc`, `assocOfMapSMul`, `equiv`, `map`	14
Theorems `algHom_ext`, `cancelBaseChangeAlg_symm_tmul`, `cancelBaseChangeAlg_tmul`, `cancelBaseChangeAux_symm_tmul`, `cancelBaseChange_symm_comp_lTensor`, `cancelBaseChange_symm_tmul`, `cancelBaseChange_tmul`, `comm`, `comp_iff`, `equiv_symm_algebraMap_left`, `equiv_symm_algebraMap_right`, `equiv_tmul`, `of_equiv`, `out`, `tensorProduct_tensorProduct`, `toLinearEquiv_cancelBaseChangeAlg`, `isPushout_iff`, `lift_algHom_comp_left`, `lift_algHom_comp_right`, `pushoutDesc_apply`, `pushoutDesc_left`, `pushoutDesc_right`, `algHom_ext`, `algHom_ext'`, `comp`, `comp_iff`, `equiv_symm_apply`, `equiv_tmul`, `iff_lift_unique`, `inductionOn`, `lift_comp`, `lift_eq`, `linearMap`, `map_id_lsmul_eq_lsmul_algebraMap`, `ofEquiv`, `of_comp`, `of_equiv`, `of_lift_unique`, `assocOfMapSMul_symm_tmul`, `assocOfMapSMul_tmul`, `assoc_symm_tmul`, `assoc_tmul`, `equiv_apply`, `equiv_symm_apply`, `equiv_toLinearMap`, `inductionOn`, `lift_eq`, `map_comp`, `map_eq`, `map_id`, `map_map`, `map_mul`, `map_one`, `map_pow`, `of_equiv`, `isBaseChange`, `isPushout`, `isPushout'`, `isTensorProduct`, `instIsPushout`, `instIsPushout_1`, `isBaseChange_tensorProduct_map`	62
Total	76

Algebra

Definitions

Name	Category	Theorems
`IsPushout` 📖	CompData	27 math math: `isPushout_of_isLocalization`, `MonoidAlgebra.instIsPushout`, `instIsPushoutFractionRingPolynomial_1`, `IsPushout.comm`, `instIsPushoutPolynomial_1`, `IsAlgebraic.instIsPushout`, `IsAlgebraic.instIsPushout_1`, `isPushout_iff`, `TensorProduct.isPushout`, `IsPushout.comp_iff`, `AddMonoidAlgebra.instIsPushout`, `AddMonoidAlgebra.instIsPushout'`, `CommRingCat.isPushout_iff_isPushout`, `instIsPushoutPolynomial`, `MonoidAlgebra.instIsPushout'`, `IsPushout.tensorProduct_tensorProduct`, `IsPushout.of_equiv`, `instIsPushout_1`, `instIsPushoutFractionRingPolynomial`, `MvPolynomial.instIsPushout_1`, `MvPolynomial.instIsPushout`, `instIsPushout`, `TensorProduct.isPushout'`, `IsPushout.symm`, `instIsPushoutFractionRingMvPolynomial_1`, `isLocalization_iff_isPushout`, `instIsPushoutFractionRingMvPolynomial`
`pushoutDesc` 📖	CompOp	5 math math: `pushoutDesc_right`, `lift_algHom_comp_left`, `pushoutDesc_apply`, `lift_algHom_comp_right`, `pushoutDesc_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPushout_iff` 📖	mathematical	—	`IsPushout` `IsBaseChange` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `toModule` `AlgHom.toLinearMap` `IsScalarTower.toAlgHom`	—	—
`lift_algHom_comp_left` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike`	`AlgHom.comp` `CommSemiring.toSemiring` `pushoutDesc` `IsScalarTower.toAlgHom`	—	`AlgHom.ext` `pushoutDesc_left`
`lift_algHom_comp_right` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike`	`AlgHom.comp` `CommSemiring.toSemiring` `pushoutDesc` `IsScalarTower.toAlgHom`	—	`AlgHom.ext` `pushoutDesc_right`
`pushoutDesc_apply` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike`	`DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike` `pushoutDesc` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toModule` `TensorProduct.instSemiring` `TensorProduct.leftAlgebra` `TensorProduct.lift` `id` `AlgEquiv` `AlgEquiv.instFunLike` `AlgEquiv.symm` `IsPushout.equiv`	—	—
`pushoutDesc_left` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike`	`DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike` `pushoutDesc` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`AlgEquiv.commutes` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `mul_one`
`pushoutDesc_right` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike`	`DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike` `pushoutDesc` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsPushout.equiv_symm_algebraMap_right` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `one_mul`

Algebra.IsPushout

Definitions

Name	Category	Theorems
`cancelBaseChange` 📖	CompOp	3 math math: `cancelBaseChange_tmul`, `cancelBaseChange_symm_tmul`, `toLinearEquiv_cancelBaseChangeAlg`
`cancelBaseChangeAlg` 📖	CompOp	4 math math: `cancelBaseChangeAlg_tmul`, `cancelBaseChange_symm_comp_lTensor`, `cancelBaseChangeAlg_symm_tmul`, `toLinearEquiv_cancelBaseChangeAlg`
`cancelBaseChangeAux` 📖	CompOp	1 math math: `cancelBaseChangeAux_symm_tmul`
`equiv` 📖	CompOp	4 math math: `equiv_symm_algebraMap_left`, `Algebra.pushoutDesc_apply`, `equiv_tmul`, `equiv_symm_algebraMap_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algHom_ext` 📖	—	`AlgHom.comp` `CommSemiring.toSemiring` `IsScalarTower.toAlgHom`	—	—	`AlgHom.ext` `IsBaseChange.inductionOn` `out` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.congr_fun` `Algebra.smul_def` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass`
`cancelBaseChangeAlg_symm_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommRing.toCommSemiring` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `instSMulCommClass` `AlgEquiv.instFunLike` `AlgEquiv.symm` `cancelBaseChangeAlg` `TensorProduct.tmul` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`Algebra.to_smulCommClass` `instSMulCommClass` `cancelBaseChange_symm_tmul`
`cancelBaseChangeAlg_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `instSMulCommClass` `Algebra.id` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `cancelBaseChangeAlg` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`instSMulCommClass` `Algebra.to_smulCommClass` `cancelBaseChange_tmul`
`cancelBaseChangeAux_symm_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommRing.toCommSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass'` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `cancelBaseChangeAux` `TensorProduct.tmul` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass'` `Algebra.to_smulCommClass` `equiv_tmul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul`
`cancelBaseChange_symm_comp_lTensor` 📖	mathematical	—	`AlgHom.comp` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Algebra.toModule` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.rightAlgebra` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `Algebra.to_smulCommClass` `instSMulCommClass` `AlgEquiv.toAlgHom` `AlgEquiv.symm` `cancelBaseChangeAlg` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.right_isScalarTower` `TensorProduct.isScalarTower_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `TensorProduct.isPushout` `Algebra.TensorProduct.lTensor` `IsScalarTower.toAlgHom` `Algebra.TensorProduct.includeLeft`	—	`Algebra.TensorProduct.ext_ring` `Algebra.to_smulCommClass` `instSMulCommClass` `IsScalarTower.to_smulCommClass'` `Algebra.TensorProduct.right_isScalarTower` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `IsScalarTower.to_smulCommClass` `TensorProduct.isPushout` `AlgHom.ext` `cancelBaseChangeAlg_symm_tmul`
`cancelBaseChange_symm_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommRing.toCommSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `instSMulCommClass` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `cancelBaseChange` `TensorProduct.tmul` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`cancelBaseChangeAux_symm_tmul`
`cancelBaseChange_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `instSMulCommClass` `Semiring.toModule` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `cancelBaseChange` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHomInvPair.ids` `instSMulCommClass` `Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass'` `map_one` `MonoidHomClass.toOneHomClass` `IsScalarTower.right` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `one_smul`
`comm` 📖	mathematical	—	`Algebra.IsPushout`	—	`symm`
`comp_iff` 📖	mathematical	—	`Algebra.IsPushout`	—	`RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.of_algebraMap_eq` `IsScalarTower.algebraMap_apply` `LinearMap.ext` `Algebra.isPushout_iff` `IsBaseChange.comp_iff` `out`
`equiv_symm_algebraMap_left` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `AlgEquiv.symm` `equiv` `RingHom` `RingHom.instFunLike` `algebraMap` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Algebra.to_smulCommClass` `AlgEquiv.symm_apply_eq` `equiv_tmul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_one`
`equiv_symm_algebraMap_right` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `AlgEquiv.symm` `equiv` `RingHom` `RingHom.instFunLike` `algebraMap` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Algebra.to_smulCommClass` `AlgEquiv.symm_apply_eq` `equiv_tmul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul`
`equiv_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `equiv` `TensorProduct.tmul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `out` `IsBaseChange.equiv_tmul` `Algebra.smul_def`
`of_equiv` 📖	mathematical	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingEquiv.toRingHom` `AlgEquiv.toRingEquiv` `algebraMap`	`Algebra.IsPushout`	—	`Algebra.isPushout_iff` `IsBaseChange.of_equiv` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `one_smul` `DFunLike.congr_fun`
`out` 📖	mathematical	—	`IsBaseChange` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `AlgHom.toLinearMap` `IsScalarTower.toAlgHom`	—	—
`tensorProduct_tensorProduct` 📖	mathematical	`RingHom.comp` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instCommSemiring` `Algebra.TensorProduct.instSemiring` `algebraMap` `AlgHom.toRingHom` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight`	`Algebra.IsPushout` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instCommSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `TensorProduct.isScalarTower_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `IsScalarTower.right`	—	`Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `TensorProduct.AlgebraTensorModule.curry_injective` `LinearMap.ext_ring` `LinearMap.ext` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `isBaseChange_tensorProduct_map` `IsBaseChange.linearMap`
`toLinearEquiv_cancelBaseChangeAlg` 📖	mathematical	—	`AlgEquiv.toLinearEquiv` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `instSMulCommClass` `Algebra.id` `Algebra.to_smulCommClass` `cancelBaseChangeAlg` `cancelBaseChange` `Ring.toAddCommGroup` `CommRing.toRing`	—	`RingHomInvPair.ids` `instSMulCommClass` `Algebra.to_smulCommClass`

IsBaseChange

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	5 math math: `equiv_symm_apply`, `endHom_apply`, `toDual_apply`, `equiv_tmul`, `linearMapLeftRightHom_apply`
`tensorEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algHom_ext` 📖	—	`IsBaseChange` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	—	`LinearMap.ext` `inductionOn` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.map_smul` `map_add` `SemilinearMapClass.toAddHomClass`
`algHom_ext'` 📖	—	`IsBaseChange` `LinearMap.comp` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.restrictScalars` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul`	—	—	`RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `algHom_ext` `LinearMap.congr_fun`
`comp` 📖	mathematical	`IsBaseChange`	`IsBaseChange` `LinearMap.comp` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.restrictScalars` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul`	—	`of_lift_unique` `RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.to₁₂₄` `Algebra.smul_def` `SemigroupAction.mul_smul` `LinearMap.ext` `lift_eq` `algHom_ext'` `lift_comp`
`comp_iff` 📖	mathematical	`IsBaseChange`	`IsBaseChange` `LinearMap.comp` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.restrictScalars` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul`	—	`RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `of_comp` `comp`
`equiv_symm_apply` 📖	mathematical	`IsBaseChange`	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `equiv` `LinearMap` `LinearMap.instFunLike` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `LinearEquiv.symm_apply_eq` `equiv_tmul` `one_smul`
`equiv_tmul` 📖	mathematical	`IsBaseChange`	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `equiv` `TensorProduct.tmul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `LinearMap` `LinearMap.instFunLike`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`iff_lift_unique` 📖	mathematical	—	`IsBaseChange` `ExistsUnique` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.comp` `RingHomCompTriple.ids` `LinearMap.restrictScalars` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul`	—	`RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `lift_comp` `algHom_ext'` `of_lift_unique`
`inductionOn` 📖	—	`IsBaseChange` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`IsTensorProduct.inductionOn`
`lift_comp` 📖	mathematical	`IsBaseChange`	`LinearMap.comp` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.restrictScalars` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `lift`	—	`LinearMap.ext` `RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `lift_eq`
`lift_eq` 📖	mathematical	`IsBaseChange`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `lift`	—	`IsTensorProduct.lift_eq` `one_smul`
`linearMap` 📖	mathematical	—	`IsBaseChange` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `Algebra.toModule` `IsScalarTower.right` `Algebra.linearMap`	—	`of_equiv` `IsScalarTower.right` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `Algebra.algebraMap_eq_smul_one`
`map_id_lsmul_eq_lsmul_algebraMap` 📖	mathematical	`IsBaseChange`	`IsTensorProduct.map` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `LinearMap.restrictScalars` `LinearMap` `RingHom.id` `LinearMap.addCommMonoid` `LinearMap.module` `Semiring.toModule` `DFunLike.coe` `LinearMap.instFunLike` `LinearMap.flip` `Algebra.linearMap` `Module.End` `Module.End.instSemiring` `Module.End.instAlgebra` `Algebra.toSMul` `Algebra.id` `LinearMap.id` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.lsmul` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`LinearMap.ext` `smulCommClass_self` `LinearMap.IsScalarTower.compatibleSMul` `IsTensorProduct.inductionOn` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `smul_zero` `IsTensorProduct.map_eq` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `algebraMap_smul` `SMulCommClass.smul_comm` `IsScalarTower.to_smulCommClass` `map_add` `SemilinearMapClass.toAddHomClass` `smul_add`
`ofEquiv` 📖	mathematical	—	`IsBaseChange` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `of_lift_unique` `IsScalarTower.left` `Module.ext` `one_smul` `smul_smul` `smul_assoc` `smul_eq_mul` `RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `LinearMap.ext` `LinearEquiv.symm_apply_apply` `LinearEquiv.apply_symm_apply`
`of_comp` 📖	mathematical	`IsBaseChange` `LinearMap.comp` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.restrictScalars` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul`	`IsBaseChange`	—	`RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `of_lift_unique` `IsScalarTower.restrictScalars` `IsScalarTower.of_algebraMap_smul` `IsScalarTower.algebraMap_apply` `algebraMap_smul` `algHom_ext'` `lift_comp` `LinearMap.comp_assoc`
`of_equiv` 📖	mathematical	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `LinearMap` `LinearMap.instFunLike`	`IsBaseChange`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `IsTensorProduct.of_equiv` `LinearMap.IsScalarTower.compatibleSMul` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `mul_one` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`of_lift_unique` 📖	mathematical	`ExistsUnique` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.comp` `RingHomCompTriple.ids` `LinearMap.restrictScalars` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul`	`IsBaseChange`	—	`RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `Algebra.to_smulCommClass` `ULift.isScalarTower''` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `RingHomInvPair.ids` `TensorProduct.smulCommClass_left` `smulCommClass_self` `IsScalarTower.to_smulCommClass` `LinearMap.IsScalarTower.compatibleSMul'` `LinearMap.instIsScalarTower` `SMulCommClass.symm` `LinearMap.instSMulCommClass` `IsScalarTower.left` `TensorProduct.induction_on` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `smul_zero` `smul_assoc` `smul_add` `map_add` `SemilinearMapClass.toAddHomClass` `RingHomInvPair.triples₂` `LinearMap.cancel_left` `LinearEquiv.injective` `ExistsUnique.unique` `LinearMap.ext` `ULift.ext` `one_smul` `TensorProduct.AlgebraTensorModule.curry_injective` `LinearMap.ext_ring` `LinearEquiv.bijective`

IsTensorProduct

Definitions

Name	Category	Theorems
`assoc` 📖	CompOp	2 math math: `assoc_symm_tmul`, `assoc_tmul`
`assocOfMapSMul` 📖	CompOp	2 math math: `assocOfMapSMul_symm_tmul`, `assocOfMapSMul_tmul`
`equiv` 📖	CompOp	3 math math: `equiv_symm_apply`, `equiv_apply`, `equiv_toLinearMap`
`map` 📖	CompOp	12 math math: `map_id_injective_of_flat_left`, `map_map`, `map_pow`, `map_injective_of_flat_right_left`, `map_one`, `map_id_injective_of_flat_right`, `IsBaseChange.map_id_lsmul_eq_lsmul_algebraMap`, `map_injective_of_flat_left_right`, `map_id`, `map_mul`, `map_comp`, `map_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`assocOfMapSMul_symm_tmul` 📖	mathematical	`IsTensorProduct` `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` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `assocOfMapSMul` `TensorProduct.tmul` `LinearMap` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`smulCommClass_self` `assoc_symm_tmul`
`assocOfMapSMul_tmul` 📖	mathematical	`IsTensorProduct` `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` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `assocOfMapSMul` `TensorProduct.tmul` `LinearMap` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`smulCommClass_self` `assoc_tmul`
`assoc_symm_tmul` 📖	mathematical	`IsTensorProduct` `LinearMap.restrictScalars₁₂` `CommSemiring.toSemiring` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.toSMul`	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `assoc` `TensorProduct.tmul` `LinearMap` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`smulCommClass_self` `IsScalarTower.to_smulCommClass'` `IsScalarTower.left`
`assoc_tmul` 📖	mathematical	`IsTensorProduct` `LinearMap.restrictScalars₁₂` `CommSemiring.toSemiring` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.toSMul`	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `assoc` `TensorProduct.tmul` `LinearMap` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`smulCommClass_self` `IsScalarTower.to_smulCommClass'` `IsScalarTower.left`
`equiv_apply` 📖	mathematical	`IsTensorProduct`	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `equiv` `LinearMap` `LinearMap.instFunLike` `TensorProduct.lift`	—	`smulCommClass_self` `RingHomInvPair.ids`
`equiv_symm_apply` 📖	mathematical	`IsTensorProduct`	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `equiv` `LinearMap` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorProduct.tmul`	—	`smulCommClass_self` `LinearEquiv.injective` `RingHomInvPair.ids` `LinearEquiv.apply_symm_apply`
`equiv_toLinearMap` 📖	mathematical	`IsTensorProduct`	`LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `equiv` `TensorProduct.lift`	—	`smulCommClass_self` `RingHomInvPair.ids`
`inductionOn` 📖	—	`IsTensorProduct` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Module.toDistribMulAction` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`smulCommClass_self` `RingHomInvPair.ids` `LinearEquiv.right_inv` `TensorProduct.induction_on` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `TensorProduct.lift.tmul` `map_add` `SemilinearMapClass.toAddHomClass`
`lift_eq` 📖	mathematical	`IsTensorProduct`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `lift` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`smulCommClass_self` `equiv_symm_apply`
`map_comp` 📖	mathematical	`IsTensorProduct`	`map` `LinearMap.comp` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`smulCommClass_self` `LinearMap.ext` `RingHomCompTriple.ids` `inductionOn` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_eq` `map_add` `SemilinearMapClass.toAddHomClass`
`map_eq` 📖	mathematical	`IsTensorProduct`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `map` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`smulCommClass_self` `equiv_symm_apply`
`map_id` 📖	mathematical	`IsTensorProduct`	`map` `LinearMap.id` `CommSemiring.toSemiring`	—	`smulCommClass_self` `LinearMap.ext` `inductionOn` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_eq` `map_add` `SemilinearMapClass.toAddHomClass`
`map_map` 📖	mathematical	`IsTensorProduct`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `map` `LinearMap.comp` `RingHomCompTriple.ids`	—	`smulCommClass_self` `DFunLike.congr_fun` `RingHomCompTriple.ids` `map_comp`
`map_mul` 📖	mathematical	`IsTensorProduct`	`map` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End.instMul`	—	`smulCommClass_self` `map_comp`
`map_one` 📖	mathematical	`IsTensorProduct`	`map` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End.instOne`	—	`smulCommClass_self` `map_id`
`map_pow` 📖	mathematical	`IsTensorProduct`	`LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toPow` `Module.End.instMonoid` `map`	—	`smulCommClass_self` `pow_zero` `map.congr_simp` `map_one` `pow_succ` `map_mul`
`of_equiv` 📖	mathematical	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `TensorProduct.tmul` `LinearMap` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	`IsTensorProduct`	—	`smulCommClass_self` `RingHomInvPair.ids` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `LinearEquiv.bijective`

TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBaseChange` 📖	mathematical	—	`IsBaseChange` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `addCommMonoid` `instModule` `leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `isScalarTower_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `IsScalarTower.right` `DFunLike.coe` `LinearMap` `RingHom.id` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_left` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `LinearMap.instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Algebra.to_smulCommClass` `isScalarTower_left` `IsScalarTower.right` `smulCommClass_left` `smulCommClass_self` `LinearMap.ext` `smul_tmul'` `mul_one` `isTensorProduct`
`isPushout` 📖	mathematical	—	`Algebra.IsPushout` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instCommSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `Algebra.TensorProduct.rightAlgebra` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.right_isScalarTower` `isScalarTower_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `IsScalarTower.right`	—	`Algebra.to_smulCommClass` `Algebra.TensorProduct.right_isScalarTower` `isScalarTower_left` `IsScalarTower.right` `isBaseChange`
`isPushout'` 📖	mathematical	—	`Algebra.IsPushout` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instCommSemiring` `Algebra.TensorProduct.rightAlgebra` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `Algebra.TensorProduct.instAlgebra` `isScalarTower_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `IsScalarTower.right` `Algebra.TensorProduct.right_isScalarTower`	—	`Algebra.IsPushout.symm` `Algebra.to_smulCommClass` `Algebra.TensorProduct.right_isScalarTower` `isScalarTower_left` `IsScalarTower.right` `isPushout`
`isTensorProduct` 📖	mathematical	—	`IsTensorProduct` `TensorProduct` `addCommMonoid` `instModule`	—	`ext'` `Function.bijective_id`

(root)

Definitions

Name	Category	Theorems
`IsBaseChange` 📖	MathDef	29 math math: `IsBaseChange.comp_iff`, `IsBaseChange.finsuppPow`, `IsLocalizedModule.isBaseChange`, `IsBaseChange.of_lift_unique`, `isLocalizedModule_iff_isBaseChange`, `IsBaseChange.of_comp`, `IsBaseChange.directSumPow`, `IsBaseChange.directSum`, `isBaseChange_tensorProduct_map`, `IsBaseChange.of_basis`, `IsBaseChange.of_fintype_basis`, `Algebra.isPushout_iff`, `IsBaseChange.pi`, `IsBaseChange.prodMap`, `IsBaseChange.end`, `Algebra.IsPushout.out`, `KaehlerDifferential.isBaseChange`, `IsBaseChange.of_equiv`, `TensorProduct.isBaseChange`, `IsBaseChange.iff_lift_unique`, `Algebra.IsAlgebraic.isBaseChange_of_isFractionRing`, `IsBaseChange.ofEquiv`, `IsBaseChange.dual`, `IsBaseChange.linearMapLeftRight`, `KaehlerDifferential.isBaseChange_of_formallyEtale`, `IsBaseChange.linearMap`, `IsBaseChange.comp`, `IsBaseChange.linearMapRight`, `IsBaseChange.finitePow`
`IsTensorProduct` 📖	MathDef	2 math math: `IsTensorProduct.of_equiv`, `TensorProduct.isTensorProduct`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsPushout` 📖	mathematical	—	`Algebra.IsPushout` `Algebra.id` `IsScalarTower.right` `CommSemiring.toSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.right` `IsScalarTower.left` `IsBaseChange.of_equiv` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `one_smul`
`instIsPushout_1` 📖	mathematical	—	`Algebra.IsPushout` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `Algebra.toModule` `IsScalarTower.right`	—	`Algebra.IsPushout.symm` `IsScalarTower.right` `IsScalarTower.left` `instIsPushout`
`isBaseChange_tensorProduct_map` 📖	mathematical	`IsBaseChange`	`IsBaseChange` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `CommSemiring.toSemiring` `IsScalarTower.to_smulCommClass` `TensorProduct.isScalarTower_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `TensorProduct.AlgebraTensorModule.map` `LinearMap.id`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass` `Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass'` `TensorProduct.smulCommClass_left` `IsScalarTower.right` `RingHomCompTriple.ids` `TensorProduct.isScalarTower_left` `IsBaseChange.of_equiv` `TensorProduct.induction_on` `TensorProduct.tmul_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearMap.semilinearMapClass` `one_smul` `TensorProduct.tmul_add` `map_add` `SemilinearMapClass.toAddHomClass`

---

← Back to Index