Map

📁 Source: Mathlib/LinearAlgebra/TensorProduct/Map.lean

Statistics

Metric	Count
Definitions `lTensor`, `rTensor`, `lTensor`, `lTensorHom`, `rTensor`, `rTensorHom`, `«term_⊗ₘ_»`, `homTensorHomMap`, `lTensorHomToHomLTensor`, `map`, `mapBilinear`, `mapIncl`, `map₂`, `rTensorHomToHomRTensor`	14
Theorems `tensorProductComm_def`, `coe_lTensor`, `coe_lTensor_symm`, `coe_rTensor`, `coe_rTensor_symm`, `comm_trans_lTensor_trans_comm_eq`, `comm_trans_rTensor_trans_comm_eq`, `congr_trans_lTensor`, `congr_trans_rTensor`, `lTensor_mul`, `lTensor_pow`, `lTensor_refl`, `lTensor_refl_apply`, `lTensor_symm_tmul`, `lTensor_tmul`, `lTensor_trans`, `lTensor_trans_apply`, `lTensor_trans_congr`, `lTensor_trans_rTensor`, `lTensor_zpow`, `rTensor_mul`, `rTensor_pow`, `rTensor_refl`, `rTensor_refl_apply`, `rTensor_symm_tmul`, `rTensor_tmul`, `rTensor_trans`, `rTensor_trans_apply`, `rTensor_trans_congr`, `rTensor_trans_lTensor`, `rTensor_zpow`, `coe_lTensorHom`, `coe_rTensorHom`, `comm_comp_lTensor_comp_comm_eq`, `comm_comp_rTensor_comp_comm_eq`, `lTensor_add`, `lTensor_bij_iff_rTensor_bij`, `lTensor_comm`, `lTensor_comp`, `lTensor_comp_apply`, `lTensor_comp_comm`, `lTensor_comp_map`, `lTensor_comp_mk`, `lTensor_comp_rTensor`, `lTensor_def`, `lTensor_id`, `lTensor_id_apply`, `lTensor_inj_iff_rTensor_inj`, `lTensor_map`, `lTensor_mul`, `lTensor_neg`, `lTensor_pow`, `lTensor_smul`, `lTensor_smul_action`, `lTensor_sub`, `lTensor_surj_iff_rTensor_surj`, `lTensor_tmul`, `lTensor_zero`, `map_comp_lTensor`, `map_comp_rTensor`, `map_lTensor`, `map_rTensor`, `rTensor_add`, `rTensor_comm`, `rTensor_comp`, `rTensor_comp_apply`, `rTensor_comp_comm`, `rTensor_comp_flip_mk`, `rTensor_comp_lTensor`, `rTensor_comp_map`, `rTensor_def`, `rTensor_id`, `rTensor_id_apply`, `rTensor_map`, `rTensor_mul`, `rTensor_neg`, `rTensor_pow`, `rTensor_smul`, `rTensor_smul_action`, `rTensor_sub`, `rTensor_tmul`, `rTensor_zero`, `smul_lTensor`, `congr_congr`, `congr_mul`, `congr_pow`, `congr_refl_refl`, `congr_symm`, `congr_symm_tmul`, `congr_tmul`, `congr_trans`, `congr_zpow`, `homTensorHomMap_apply`, `instSmall`, `lTensorHomToHomLTensor_apply`, `lift_comp_map`, `mapBilinear_apply`, `map_add_left`, `map_add_right`, `map_bijective`, `map_comm`, `map_comp`, `map_comp_comm_eq`, `map_id`, `map_map`, `map_mul`, `map_one`, `map_pow`, `map_range_eq_span_tmul`, `map_smul_left`, `map_smul_right`, `map_tmul`, `map_zero_left`, `map_zero_right`, `map₂_apply_tmul`, `map₂_eq_range_lift_comp_mapIncl`, `rTensorHomToHomRTensor_apply`, `range_map`, `range_mapIncl`, `range_mapIncl_mono`, `range_map_eq_span_tmul`, `range_map_mono`, `toLinearMap_congr`	123
Total	137

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tensorProductComm_def` 📖	mathematical	—	`TensorProduct.comm` `addCommMonoid` `module` `CommSemiring.toSemiring` `LinearEquiv.trans` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `TensorProduct.congr` `linearEquiv` `LinearEquiv.symm`	—	`LinearEquiv.ext` `RingHomInvPair.ids` `RingHomCompTriple.ids` `TensorProduct.induction_on` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearEquiv.symm_apply_apply` `map_add` `SemilinearMapClass.toAddHomClass`

LinearEquiv

Definitions

Name	Category	Theorems
`lTensor` 📖	CompOp	22 math math: `lTensor_pow`, `LinearIsometryEquiv.lTensor_apply`, `coe_lTensor`, `comm_trans_lTensor_trans_comm_eq`, `lTensor_zpow`, `lTensor_trans_congr`, `lTensor_tmul`, `LinearIsometryEquiv.toLinearEquiv_lTensor`, `lTensor_refl`, `TensorProduct.assoc_tensor''`, `coe_lTensor_symm`, `comm_trans_rTensor_trans_comm_eq`, `lTensor_trans_apply`, `lTensor_symm_tmul`, `rTensor_trans_lTensor`, `TensorProduct.assoc_tensor`, `lTensor_refl_apply`, `TensorProduct.assoc_tensor'`, `lTensor_trans_rTensor`, `lTensor_trans`, `lTensor_mul`, `congr_trans_lTensor`
`rTensor` 📖	CompOp	23 math math: `rTensor_mul`, `comm_trans_lTensor_trans_comm_eq`, `rTensor_trans_congr`, `rTensor_zpow`, `rTensor_refl_apply`, `rTensor_pow`, `congr_trans_rTensor`, `rTensor_refl`, `rTensor_symm_tmul`, `LinearIsometryEquiv.rTensor_apply`, `TensorProduct.assoc_tensor''`, `coe_rTensor_symm`, `rTensor_trans_apply`, `comm_trans_rTensor_trans_comm_eq`, `LinearIsometryEquiv.toLinearEquiv_rTensor`, `rTensor_trans_lTensor`, `TensorProduct.assoc_tensor`, `rTensor_trans`, `TensorProduct.assoc_tensor'`, `lTensor_trans_rTensor`, `rTensor_tmul`, `TensorProduct.lid_tensor`, `coe_rTensor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_lTensor` 📖	mathematical	—	`toLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `lTensor` `LinearMap.lTensor`	—	`RingHomInvPair.ids`
`coe_lTensor_symm` 📖	mathematical	—	`toLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `symm` `lTensor` `LinearMap.lTensor`	—	`RingHomInvPair.ids`
`coe_rTensor` 📖	mathematical	—	`toLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `rTensor` `LinearMap.rTensor`	—	`RingHomInvPair.ids`
`coe_rTensor_symm` 📖	mathematical	—	`toLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `symm` `rTensor` `LinearMap.rTensor`	—	`RingHomInvPair.ids`
`comm_trans_lTensor_trans_comm_eq` 📖	mathematical	—	`trans` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `TensorProduct.comm` `lTensor` `rTensor`	—	`RingHomInvPair.ids` `toLinearMap_injective` `RingHomCompTriple.ids` `TensorProduct.ext` `smulCommClass_self`
`comm_trans_rTensor_trans_comm_eq` 📖	mathematical	—	`trans` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `TensorProduct.comm` `rTensor` `lTensor`	—	`RingHomInvPair.ids` `toLinearMap_injective` `RingHomCompTriple.ids` `TensorProduct.ext` `smulCommClass_self`
`congr_trans_lTensor` 📖	mathematical	—	`trans` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `TensorProduct.congr` `lTensor`	—	`RingHomInvPair.ids` `toLinearMap_injective` `RingHomCompTriple.ids` `LinearMap.lTensor_comp_map`
`congr_trans_rTensor` 📖	mathematical	—	`trans` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `TensorProduct.congr` `rTensor`	—	`RingHomInvPair.ids` `toLinearMap_injective` `RingHomCompTriple.ids` `LinearMap.rTensor_comp_map`
`lTensor_mul` 📖	mathematical	—	`lTensor` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `automorphismGroup` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`RingHomInvPair.ids` `lTensor_trans`
`lTensor_pow` 📖	mathematical	—	`LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `automorphismGroup` `lTensor`	—	`RingHomInvPair.ids` `one_pow` `TensorProduct.congr_pow`
`lTensor_refl` 📖	mathematical	—	`lTensor` `refl` `CommSemiring.toSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`TensorProduct.congr_refl_refl`
`lTensor_refl_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `instEquivLike` `lTensor` `refl`	—	`RingHomInvPair.ids` `lTensor_refl` `refl_apply`
`lTensor_symm_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `instEquivLike` `symm` `lTensor` `TensorProduct.tmul`	—	`RingHomInvPair.ids`
`lTensor_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `instEquivLike` `lTensor` `TensorProduct.tmul`	—	`RingHomInvPair.ids`
`lTensor_trans` 📖	mathematical	—	`lTensor` `trans` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`RingHomInvPair.ids` `toLinearMap_injective` `RingHomCompTriple.ids` `LinearMap.lTensor_comp`
`lTensor_trans_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `instEquivLike` `lTensor` `trans` `RingHomCompTriple.ids`	—	`RingHomInvPair.ids` `LinearMap.lTensor_comp_apply`
`lTensor_trans_congr` 📖	mathematical	—	`trans` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `lTensor` `TensorProduct.congr`	—	`RingHomInvPair.ids` `toLinearMap_injective` `RingHomCompTriple.ids` `LinearMap.map_comp_lTensor`
`lTensor_trans_rTensor` 📖	mathematical	—	`trans` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `lTensor` `rTensor` `TensorProduct.congr`	—	`RingHomInvPair.ids` `toLinearMap_injective` `RingHomCompTriple.ids` `LinearMap.rTensor_comp_lTensor`
`lTensor_zpow` 📖	mathematical	—	`LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `automorphismGroup` `lTensor`	—	`RingHomInvPair.ids` `one_zpow` `TensorProduct.congr_zpow`
`rTensor_mul` 📖	mathematical	—	`rTensor` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `automorphismGroup` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`RingHomInvPair.ids` `rTensor_trans`
`rTensor_pow` 📖	mathematical	—	`LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `automorphismGroup` `rTensor`	—	`RingHomInvPair.ids` `one_pow` `TensorProduct.congr_pow`
`rTensor_refl` 📖	mathematical	—	`rTensor` `refl` `CommSemiring.toSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`TensorProduct.congr_refl_refl`
`rTensor_refl_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `instEquivLike` `rTensor` `refl`	—	`RingHomInvPair.ids` `rTensor_refl` `refl_apply`
`rTensor_symm_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `instEquivLike` `symm` `rTensor` `TensorProduct.tmul`	—	`RingHomInvPair.ids`
`rTensor_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `instEquivLike` `rTensor` `TensorProduct.tmul`	—	`RingHomInvPair.ids`
`rTensor_trans` 📖	mathematical	—	`rTensor` `trans` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`RingHomInvPair.ids` `toLinearMap_injective` `RingHomCompTriple.ids` `LinearMap.rTensor_comp`
`rTensor_trans_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `instEquivLike` `rTensor` `trans` `RingHomCompTriple.ids`	—	`RingHomInvPair.ids` `LinearMap.rTensor_comp_apply`
`rTensor_trans_congr` 📖	mathematical	—	`trans` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `rTensor` `TensorProduct.congr`	—	`RingHomInvPair.ids` `toLinearMap_injective` `RingHomCompTriple.ids` `LinearMap.map_comp_rTensor`
`rTensor_trans_lTensor` 📖	mathematical	—	`trans` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `rTensor` `lTensor` `TensorProduct.congr`	—	`RingHomInvPair.ids` `toLinearMap_injective` `RingHomCompTriple.ids` `LinearMap.lTensor_comp_rTensor`
`rTensor_zpow` 📖	mathematical	—	`LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `automorphismGroup` `rTensor`	—	`RingHomInvPair.ids` `one_zpow` `TensorProduct.congr_zpow`

LinearMap

Definitions

Name	Category	Theorems
`lTensor` 📖	CompOp	121 math math: `TensorProduct.finsuppRight_apply`, `lTensor_ker_subtype_tensorKerEquiv_symm`, `lTensor.inverse_comp_lTensor`, `baseChange_eq_ltensor`, `Module.Flat.iff_lTensor_exact'`, `Coalgebra.lTensor_counit_comul`, `Module.FaithfullyFlat.iff_exact_iff_lTensor_exact`, `lTensor_sub`, `rTensor_comm`, `Module.FaithfullyFlat.lTensor_injective_iff_injective`, `lTensor_rTensor_comp_assoc`, `Module.Flat.lTensor_preserves_injective_linearMap`, `Coalgebra.coassoc_symm_apply`, `lTensor.inverse_of_rightInverse_comp_lTensor`, `lTensor_id_apply`, `Module.Flat.lTensor_exact`, `Module.FaithfullyFlat.lTensor_exact_iff_exact`, `Module.FaithfullyFlat.lTensor_bijective_iff_bijective`, `contractLeft_assoc_coevaluation`, `Submodule.FG.lTensor.directedSystem`, `tensorKer_coe`, `lTensor_smul`, `lTensor_surj_iff_rTensor_surj`, `le_comap_range_lTensor`, `rTensor_comp_lTensor`, `LinearEquiv.coe_lTensor`, `TensorProduct.directLimitRight_tmul_of`, `TensorProduct.tensorQuotEquivQuotSMul_comp_mkQ_lTensor`, `TensorProduct.gradedMul_def`, `TensorProduct.AlgebraTensorModule.restrictScalars_lTensor`, `Finsupp.linearCombination_one_tmul`, `Module.FaithfullyFlat.lTensor_surjective_iff_surjective`, `lTensor_comp_comm`, `coe_lTensorHom`, `ModuleCat.MonoidalCategory.whiskerLeft_def`, `lTensor_range`, `Module.Flat.iff_lTensor_preserves_injective_linearMap`, `lTensor.inverse_of_rightInverse_apply`, `tensorKerEquivOfSurjective_symm_tmul`, `tensorEqLocus_coe`, `TensorProduct.finsuppScalarRight_apply`, `Algebra.FormallySmooth.iff_injective_lTensor_residueField`, `Ideal.map_includeRight_eq`, `lTensor_surjective`, `lTensor.inverse_apply`, `LinearIsometry.lTensor_apply`, `rTensor_lTensor_comp_assoc_symm`, `TensorProduct.exists_finite_submodule_right_of_setFinite`, `lTensor_exact`, `Module.Flat.iff_lTensor_exact`, `Module.Flat.iff_lTensor_preserves_injective_linearMap'`, `lTensor_smul_action`, `lTensor_neg`, `Submodule.FG.lTensor.directLimit_apply'`, `ModuleCat.hom_whiskerLeft`, `Module.FaithfullyFlat.iff_zero_iff_lTensor_zero`, `smul_lTensor`, `comm_comp_lTensor_comp_comm_eq`, `QuotSMulTop.equivQuotTensor_naturality`, `TensorProduct.exists_finite_submodule_right_of_setFinite'`, `TensorProduct.AlgebraTensorModule.coe_lTensor`, `map_comp_lTensor`, `lTensor_mul`, `Submodule.mulRightMap_eq_mulMap_comp`, `Module.Flat.iff_lTensor_injective`, `lTensor_comm`, `lTensor_id`, `rTensor_comp_comm`, `Coalgebra.coassoc`, `Module.Flat.iff_lTensor_injectiveₛ`, `SemimoduleCat.hom_whiskerLeft`, `lTensor_comp_rTensor`, `lTensor_zero`, `adjoint_lTensor`, `lTensor_comp_mk`, `IsLocalRing.split_injective_iff_lTensor_residueField_injective`, `DirectedSystem.lTensor`, `Module.FaithfullyFlat.zero_iff_lTensor_zero`, `lTensor_bij_iff_rTensor_bij`, `lTensor_comp_apply`, `QuotSMulTop.equivQuotTensor_naturality_mk`, `Module.Flat.iff_lTensor_preserves_injective_linearMapₛ`, `Module.Invertible.lTensor_injective_iff`, `TensorProduct.equivFinsuppOfBasisRight_apply`, `lTensor_injective_of_exact_of_flat`, `intrinsicStar_lTensor`, `Submodule.FG.lTensor.directLimit_apply`, `map_lTensor`, `Submodule.mulMap_comp_lTensor`, `rTensor_exact_iff_lTensor_exact`, `LinearEquiv.coe_lTensor_symm`, `TensorProduct.exists_finite_submodule_right_of_finite`, `Rep.indMap_hom`, `Module.Invertible.lTensor_surjective_iff`, `TensorProduct.exists_finite_submodule_right_of_finite'`, `Module.Invertible.lTensor_bijective_iff`, `Coalgebra.coassoc_apply`, `HopfAlgebra.mul_antipode_lTensor_comul_apply`, `Coalgebra.coassoc_symm`, `lTensor_comp`, `rid_comp_lTensor`, `TensorProduct.map_ker`, `Coalgebra.lTensor_counit_comp_comul`, `lTensor_pow`, `HopfAlgebra.mul_antipode_lTensor_comul`, `lTensor_map`, `LinearIsometry.toLinearMap_lTensor`, `lTensor_comp_map`, `TensorProduct.directLimitRight_symm_of_tmul`, `lTensor_add`, `lTensor_mkQ`, `lTensor_inj_iff_rTensor_inj`, `comm_comp_rTensor_comp_comm_eq`, `lTensor_tensor`, `TensorProduct.instDirectedSystemCoeLinearMapIdLTensor`, `Module.Flat.iff_lTensor_injective'`, `contractLeft_assoc_coevaluation'`, `lTensor_tmul`, `lTensor_def`, `lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm`, `Module.Invertible.leftCancelEquiv_comp_lTensor_comp_symm`
`lTensorHom` 📖	CompOp	1 math math: `coe_lTensorHom`
`rTensor` 📖	CompOp	143 math math: `TensorProduct.forall_vanishesTrivially_iff_forall_fg_rTensor_injective`, `Submodule.FG.rTensor.directedSystem`, `Submodule.exists_fg_le_eq_rTensor_inclusion`, `rTensor_comm`, `Module.Flat.iff_rTensor_preserves_injective_linearMap`, `lTensor_rTensor_comp_assoc`, `rTensor_smul_action`, `QuotSMulTop.equivTensorQuot_naturality`, `Coalgebra.coassoc_symm_apply`, `rTensor_injective_iff_lcomp_surjective`, `contractLeft_assoc_coevaluation`, `rTensor_id`, `TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor`, `lTensor_surj_iff_rTensor_surj`, `rTensor_id_apply`, `QuotSMulTop.equivTensorQuot_naturality_mk`, `PolynomialLaw.exists_lift'`, `PolynomialLaw.toFun_eq_rTensor_φ_toFun'`, `rTensor_comp_lTensor`, `rTensor_comp_map`, `rTensor_comp_flip_mk`, `Module.FaithfullyFlat.iff_zero_iff_rTensor_zero`, `rTensor_tmul`, `Module.Flat.out`, `TensorProduct.gradedMul_def`, `rTensor.inverse_of_rightInverse_apply`, `Module.FaithfullyFlat.zero_iff_rTensor_zero`, `lTensor_comp_comm`, `Polynomial.X_pow_smul_rTensor_monomial`, `rTensor_sub`, `Module.Flat.iff_rTensor_injective`, `TensorProduct.Algebra.exists_of_fg`, `TensorProduct.exists_finite_submodule_left_of_setFinite`, `TensorProduct.AlgebraTensorModule.rTensor_tensor`, `TensorProduct.directSumRight_comp_rTensor`, `TensorProduct.instDirectedSystemCoeLinearMapIdRTensor`, `adjoint_rTensor`, `rTensor_injective_iff_subtype`, `Module.FaithfullyFlat.rTensor_exact_iff_exact`, `rTensor_lTensor_comp_assoc_symm`, `ModuleCat.hom_whiskerRight`, `PolynomialLaw.exists_lift`, `Module.Flat.rTensor_exact`, `Module.FaithfullyFlat.iff_exact_iff_rTensor_exact`, `Submodule.FG.rTensor.directLimit_apply`, `TensorProduct.directLimitLeft_rTensor_of`, `TensorProduct.exists_finite_submodule_left_of_finite`, `intrinsicStar_rTensor`, `Submodule.exists_fg_le_subset_range_rTensor_subtype`, `TensorProduct.rTensor_injective_of_forall_vanishesTrivially`, `map_comp_rTensor`, `TensorProduct.finsuppLeft_apply`, `comm_comp_lTensor_comp_comm_eq`, `Module.Invertible.rTensor_injective_iff`, `Coalgebra.rTensor_counit_comp_comul`, `rTensor.inverse_of_rightInverse_comp_rTensor`, `TensorProduct.exists_finite_submodule_left_of_finite'`, `lTensor_comm`, `HopfAlgebra.mul_antipode_rTensor_comul`, `rTensor.inverse_comp_rTensor`, `Module.Invertible.rTensor_bijective_iff`, `map_rTensor`, `Module.Flat.iff_rTensor_exact'`, `rTensor_comp_comm`, `TensorProduct.AlgebraTensorModule.restrictScalars_rTensor`, `rTensor_baseChange`, `rTensor_mkQ`, `Coalgebra.coassoc`, `lTensor_comp_rTensor`, `TensorProduct.forall_vanishesTrivially_iff_forall_rTensor_injective`, `PolynomialLaw.isCompat`, `coe_rTensorHom`, `HopfAlgebra.mul_antipode_rTensor_comul_apply`, `Module.Flat.iff_rTensor_exact`, `rTensor_exact`, `rTensor_surjective`, `LinearIsometry.toLinearMap_rTensor`, `DirectedSystem.rTensor`, `lTensor_bij_iff_rTensor_bij`, `CharacterModule.dual_rTensor_conj_homEquiv`, `Submodule.mulLeftMap_eq_mulMap_comp`, `Submodule.exists_fg_of_baseChange_eq_zero`, `SemimoduleCat.hom_whiskerRight`, `LinearEquiv.coe_rTensor_symm`, `rTensor_map`, `Module.Invertible.rTensor_surjective_iff`, `rTensor_comp`, `rTensor_zero`, `rTensor_def`, `Ideal.pi_mkQ_rTensor`, `rTensor.inverse_apply`, `Module.Invertible.rTensorEquiv_symm_apply_apply`, `Coalgebra.rTensor_counit_comul`, `rTensor_exact_iff_lTensor_exact`, `Module.Flat.iff_rTensor_preserves_injective_linearMapₛ`, `rTensor_comp_apply`, `Submodule.exists_fg_le_subset_range_rTensor_inclusion`, `rTensor_range`, `PolynomialLaw.isCompat_apply'`, `Coalgebra.coassoc_apply`, `TensorProduct.directLimitLeft_tmul_of`, `Module.Flat.iff_rTensor_injectiveₛ`, `Coalgebra.coassoc_symm`, `Module.flat_iff`, `TensorProduct.map_ker`, `Submodule.exists_fg_le_eq_rTensor_subtype`, `TensorProduct.exists_finite_submodule_left_of_setFinite'`, `TensorProduct.directLimitLeft_symm_of_tmul`, `Submodule.map_range_rTensor_subtype_lid`, `rTensor_neg`, `PolynomialLaw.isCompat_apply`, `TensorProduct.equivFinsuppOfBasisLeft_apply`, `lid_comp_rTensor`, `MvPolynomial.rTensor_apply`, `LinearIsometry.rTensor_apply`, `TensorProduct.finsuppScalarLeft_apply`, `TensorProduct.fromDirectLimit_of_tmul`, `rTensor_add`, `Module.Invertible.rightCancelEquiv_comp_rTensor_comp_symm`, `TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor`, `rTensor_pow`, `Representation.ind_apply`, `Module.Flat.iff_rTensor_preserves_injective_linearMap'`, `rTensor_smul`, `TensorProduct.AlgebraTensorModule.coe_rTensor`, `ModuleCat.MonoidalCategory.whiskerRight_def`, `Module.Flat.iff_rTensor_injective'`, `Submodule.FG.rTensor.directLimit_apply'`, `Module.Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap`, `lTensor_inj_iff_rTensor_inj`, `comm_comp_rTensor_comp_comm_eq`, `le_comap_range_rTensor`, `Ideal.map_includeLeft_eq`, `Submodule.mulMap_comp_rTensor`, `TensorProduct.exists_of_fg`, `rTensor_mul`, `contractLeft_assoc_coevaluation'`, `LinearEquiv.coe_rTensor`, `PolynomialLaw.isCompat'`, `Module.Flat.rTensor_preserves_injective_linearMap`, `TensorProduct.toDirectLimit_tmul_of`, `rTensor_tensor`, `TensorProduct.includeRight_lid`
`rTensorHom` 📖	CompOp	2 math math: `Module.Invertible.rTensorInv_leftInverse`, `coe_rTensorHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_lTensorHom` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `addCommMonoid` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instFunLike` `lTensorHom` `lTensor`	—	`smulCommClass_self` `TensorProduct.smulCommClass_left`
`coe_rTensorHom` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `addCommMonoid` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instFunLike` `rTensorHom` `rTensor`	—	`smulCommClass_self` `TensorProduct.smulCommClass_left`
`comm_comp_lTensor_comp_comm_eq` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `TensorProduct.comm` `lTensor` `rTensor`	—	`TensorProduct.ext` `RingHomCompTriple.ids` `RingHomInvPair.ids` `smulCommClass_self`
`comm_comp_rTensor_comp_comm_eq` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `TensorProduct.comm` `rTensor` `lTensor`	—	`TensorProduct.ext` `RingHomCompTriple.ids` `RingHomInvPair.ids` `smulCommClass_self`
`lTensor_add` 📖	mathematical	—	`lTensor` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instAdd` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`map_add` `smulCommClass_self` `TensorProduct.smulCommClass_left`
`lTensor_bij_iff_rTensor_bij` 📖	mathematical	—	`Function.Bijective` `TensorProduct` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `lTensor` `rTensor`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids`
`lTensor_comm` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `lTensor` `LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `TensorProduct.comm` `rTensor`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `lTensor_comp_comm`
`lTensor_comp` 📖	mathematical	—	`lTensor` `comp` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`TensorProduct.ext` `RingHomCompTriple.ids` `ext` `smulCommClass_self`
`lTensor_comp_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `lTensor` `comp` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `lTensor_comp` `coe_comp`
`lTensor_comp_comm` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `lTensor` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `TensorProduct.comm` `rTensor`	—	`TensorProduct.map_comp_comm_eq`
`lTensor_comp_map` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `lTensor` `TensorProduct.map`	—	`RingHomCompTriple.ids`
`lTensor_comp_mk` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `lTensor` `DFunLike.coe` `LinearMap` `addCommMonoid` `module` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `instFunLike`	—	`RingHomCompTriple.ids` `TensorProduct.smulCommClass_left` `smulCommClass_self`
`lTensor_comp_rTensor` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `lTensor` `rTensor` `TensorProduct.map`	—	`RingHomCompTriple.ids`
`lTensor_def` 📖	mathematical	—	`lTensor` `TensorProduct.map` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `id`	—	—
`lTensor_id` 📖	mathematical	—	`lTensor` `id` `CommSemiring.toSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`TensorProduct.map_id`
`lTensor_id_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `lTensor` `id`	—	`lTensor_id` `id_coe`
`lTensor_inj_iff_rTensor_inj` 📖	mathematical	—	`TensorProduct` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `lTensor` `rTensor`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `EquivLike.toEmbeddingLike`
`lTensor_map` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `lTensor` `TensorProduct.map` `comp` `RingHomCompTriple.ids`	—	`congr_fun` `RingHomCompTriple.ids` `lTensor_comp_map`
`lTensor_mul` 📖	mathematical	—	`lTensor` `Module.End` `CommSemiring.toSemiring` `Module.End.instMul` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`lTensor_comp`
`lTensor_neg` 📖	mathematical	—	`lTensor` `AddCommGroup.toAddCommMonoid` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instNeg` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.addCommGroup`	—	`map_neg` `smulCommClass_self` `TensorProduct.smulCommClass_left`
`lTensor_pow` 📖	mathematical	—	`LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Monoid.toNatPow` `Module.End.instMonoid` `lTensor`	—	`TensorProduct.map_pow` `Module.End.id_pow`
`lTensor_smul` 📖	mathematical	—	`lTensor` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.instDistribMulAction` `TensorProduct.smulCommClass_left`	—	`map_smul` `smulCommClass_self` `TensorProduct.smulCommClass_left`
`lTensor_smul_action` 📖	mathematical	—	`lTensor` `DistribSMul.toLinearMap` `CommSemiring.toSemiring` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.instDistribMulAction` `TensorProduct.smulCommClass_left`	—	`smulCommClass_self` `TensorProduct.smulCommClass_left` `lTensor_smul` `lTensor_id`
`lTensor_sub` 📖	mathematical	—	`lTensor` `AddCommGroup.toAddCommMonoid` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instSub` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.addCommGroup`	—	`map_sub` `smulCommClass_self` `TensorProduct.smulCommClass_left`
`lTensor_surj_iff_rTensor_surj` 📖	mathematical	—	`TensorProduct` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `lTensor` `rTensor`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids`
`lTensor_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `lTensor` `TensorProduct.tmul`	—	—
`lTensor_zero` 📖	mathematical	—	`lTensor` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instZero` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`map_zero` `smulCommClass_self` `TensorProduct.smulCommClass_left`
`map_comp_lTensor` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `TensorProduct.map` `lTensor`	—	`RingHomCompTriple.ids`
`map_comp_rTensor` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `TensorProduct.map` `rTensor`	—	`RingHomCompTriple.ids`
`map_lTensor` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `TensorProduct.map` `lTensor` `comp` `RingHomCompTriple.ids`	—	`congr_fun` `RingHomCompTriple.ids` `map_comp_lTensor`
`map_rTensor` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `TensorProduct.map` `rTensor` `comp` `RingHomCompTriple.ids`	—	`congr_fun` `RingHomCompTriple.ids` `map_comp_rTensor`
`rTensor_add` 📖	mathematical	—	`rTensor` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instAdd` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`map_add` `smulCommClass_self` `TensorProduct.smulCommClass_left`
`rTensor_comm` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `rTensor` `LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `TensorProduct.comm` `lTensor`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `rTensor_comp_comm`
`rTensor_comp` 📖	mathematical	—	`rTensor` `comp` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`TensorProduct.ext` `RingHomCompTriple.ids` `ext` `smulCommClass_self`
`rTensor_comp_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `rTensor` `comp` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `rTensor_comp` `coe_comp`
`rTensor_comp_comm` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `rTensor` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `TensorProduct.comm` `lTensor`	—	`TensorProduct.map_comp_comm_eq`
`rTensor_comp_flip_mk` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `rTensor` `DFunLike.coe` `LinearMap` `addCommMonoid` `module` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `TensorProduct.smulCommClass_left` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `instFunLike` `flip`	—	`RingHomCompTriple.ids` `SMulCommClass.symm` `TensorProduct.smulCommClass_left` `smulCommClass_self`
`rTensor_comp_lTensor` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `rTensor` `lTensor` `TensorProduct.map`	—	`RingHomCompTriple.ids`
`rTensor_comp_map` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `rTensor` `TensorProduct.map`	—	`RingHomCompTriple.ids`
`rTensor_def` 📖	mathematical	—	`rTensor` `TensorProduct.map` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `id`	—	—
`rTensor_id` 📖	mathematical	—	`rTensor` `id` `CommSemiring.toSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`TensorProduct.map_id`
`rTensor_id_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `rTensor` `id`	—	`rTensor_id` `id_coe`
`rTensor_map` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `rTensor` `TensorProduct.map` `comp` `RingHomCompTriple.ids`	—	`congr_fun` `RingHomCompTriple.ids` `rTensor_comp_map`
`rTensor_mul` 📖	mathematical	—	`rTensor` `Module.End` `CommSemiring.toSemiring` `Module.End.instMul` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`rTensor_comp`
`rTensor_neg` 📖	mathematical	—	`rTensor` `AddCommGroup.toAddCommMonoid` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instNeg` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.addCommGroup`	—	`map_neg` `smulCommClass_self` `TensorProduct.smulCommClass_left`
`rTensor_pow` 📖	mathematical	—	`LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Monoid.toNatPow` `Module.End.instMonoid` `rTensor`	—	`TensorProduct.map_pow` `Module.End.id_pow`
`rTensor_smul` 📖	mathematical	—	`rTensor` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.instDistribMulAction` `TensorProduct.smulCommClass_left`	—	`map_smul` `smulCommClass_self` `TensorProduct.smulCommClass_left`
`rTensor_smul_action` 📖	mathematical	—	`rTensor` `DistribSMul.toLinearMap` `CommSemiring.toSemiring` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.instDistribMulAction` `TensorProduct.smulCommClass_left`	—	`smulCommClass_self` `TensorProduct.smulCommClass_left` `rTensor_smul` `rTensor_id`
`rTensor_sub` 📖	mathematical	—	`rTensor` `AddCommGroup.toAddCommMonoid` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instSub` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.addCommGroup`	—	`map_sub` `smulCommClass_self` `TensorProduct.smulCommClass_left`
`rTensor_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `rTensor` `TensorProduct.tmul`	—	—
`rTensor_zero` 📖	mathematical	—	`rTensor` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instZero` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`map_zero` `smulCommClass_self` `TensorProduct.smulCommClass_left`
`smul_lTensor` 📖	mathematical	—	`TensorProduct` `TensorProduct.leftHasSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `lTensor`	—	`TensorProduct.smulCommClass_left` `RingHomCompTriple.ids` `IsScalarTower.compatibleSMul` `TensorProduct.isScalarTower_left` `smulCommClass_self` `TensorProduct.ext`

RingTheory.LinearMap

Definitions

Name	Category	Theorems
`«term_⊗ₘ_»` 📖	CompOp	—

TensorProduct

Definitions

Name	Category	Theorems
`homTensorHomMap` 📖	CompOp	4 math math: `homTensorHomEquiv_apply`, `homTensorHomEquiv_toLinearMap`, `homTensorHomMap_apply`, `dualDistribEquivOfBasis_apply_apply`
`lTensorHomToHomLTensor` 📖	CompOp	3 math math: `lTensorHomEquivHomLTensor_apply`, `lTensorHomEquivHomLTensor_toLinearMap`, `lTensorHomToHomLTensor_apply`
`map` 📖	CompOp	127 math math: `Pi.comul_eq_adjoint`, `DFinsupp.comul_single`, `CliffordAlgebra.toBaseChange_reverse`, `Matrix.toLin_kronecker`, `LinearMap.convMul_def`, `CoalgCat.MonoidalCategoryAux.tensorHom_toLinearMap`, `AddMonoidAlgebra.comul_single`, `Pi.comul_comp_dFinsuppCoeFnLinearMap`, `tensorTensorTensorComm_comp_map`, `range_map`, `map_injective_of_flat_flat_of_isDomain`, `map_comp_comm_eq`, `map_add_right`, `map_map`, `IsLocalization.instIsLocalizedModuleTensorProductMap`, `quotientTensorQuotientEquiv_symm_apply_mk_tmul`, `Pi.comul_comp_single`, `ModuleCat.hom_tensorHom`, `adjoint_map`, `LinearMap.rTensor_comp_lTensor`, `LinearMap.rTensor_comp_map`, `exists_finite_submodule_of_finite'`, `QuadraticForm.tmul_tensorMap_apply`, `map_injective_of_flat_flat'`, `gradedMul_def`, `CoalgHom.map_comp_comul`, `Algebra.TensorProduct.linearEquivIncludeRange_toLinearMap`, `ModuleCat.MonoidalCategory.tensorHom_def`, `Representation.tprod_apply`, `AlgHom.comp_mul'`, `quotientTensorEquiv_symm_apply_mk_tmul`, `map_add_left`, `map_map_assoc_symm`, `map₂_apply_tmul`, `Finsupp.comul_comp_lapply`, `map_map_comp_assoc_eq`, `Algebra.TensorProduct.opAlgEquiv_apply`, `CoalgCat.MonoidalCategoryAux.tensorObj_comul`, `nnnorm_map`, `SemimoduleCat.hom_tensorHom`, `LinearMap.mulRight_tmul`, `intrinsicStar_map`, `LinearMap.map_comp_rTensor`, `DFinsupp.comul_comp_lapply`, `mapBilinear_apply`, `range_map_mono`, `Prod.comul_apply`, `map_comm`, `LinearMap.map_comp_lTensor`, `CoalgHomClass.map_comp_comul`, `map_smul_right`, `AlgebraTensorModule.map_eq`, `Submodule.coe_mulMap_comp_eq`, `quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk`, `tensorQuotientEquiv_apply_mk_tmul`, `map_one`, `LinearMap.map_rTensor`, `QuadraticForm.tmul_comp_tensorMap`, `lift_comp_map`, `Algebra.linearMap_comp_mul'`, `map_injective_of_flat_flat`, `toLinearMap_congr`, `LinearMap.lTensor_comp_rTensor`, `DFinsupp.comul_comp_lsingle`, `Algebra.TensorProduct.opAlgEquiv_symm_apply`, `map_mul`, `LaurentPolynomial.comul_C`, `Finsupp.comul_single`, `map_bijective`, `map_comp`, `exists_finite_submodule_of_setFinite'`, `LinearMap.trace_tensorProduct'`, `LieModule.toLinearMap_map`, `range_map_eq_span_tmul`, `LinearMap.mulLeft_tmul`, `MonoidAlgebra.comul_single`, `Pi.comul_coe_finsupp`, `NonUnitalAlgHom.comp_mul'`, `quotientTensorEquiv_apply_tmul_mk`, `map_zero_left`, `LinearMap.rTensor_map`, `LinearMap.rTensor_def`, `Prod.comul_comp_fst`, `Submodule.mulMap_map_comp_eq`, `map_tmul`, `mapIsometry_apply`, `toLinearMap_mapIsometry`, `LinearMap.map_lTensor`, `enorm_map`, `Prod.comul_comp_snd`, `Pi.comul_comp_proj`, `map_map_assoc`, `map_convMul_map`, `homTensorHomMap_apply`, `map_dualTensorHom`, `CliffordAlgebra.toBaseChange_involute`, `Pi.comul_single`, `Submodule.mulMap_comp_map_inclusion`, `MulOpposite.comul_def`, `LaurentPolynomial.comul_C_mul_T`, `Prod.comul_comp_inl`, `map_ker`, `norm_map`, `QuadraticMap.Isometry.tmul_apply`, `LinearMap.mul'_tensor`, `Pi.comul_coe_dFinsupp`, `map_smul_left`, `LinearMap.lTensor_map`, `map_map_comp_assoc_symm_eq`, `LinearMap.convMul_apply`, `Prod.comul_comp_inr`, `Finsupp.comul_comp_lsingle`, `map_range_eq_span_tmul`, `CoalgHomClass.map_comp_comul_apply`, `LinearMap.lTensor_comp_map`, `Representation.dualTensorHom_comm`, `star_map_apply_eq_map_intrinsicStar`, `map_pow`, `tensorQuotientEquiv_symm_apply_tmul_mk`, `map_surjective`, `map_id`, `map_zero_right`, `toMatrix_map`, `inner_map_map`, `LinearMap.lTensor_def`, `Pi.comul_comp_finsuppLcoeFun`, `Algebra.mul'_comp_tensorTensorTensorComm`
`mapBilinear` 📖	CompOp	2 math math: `mapBilinear_apply`, `LinearMap.trace_tensorProduct`
`mapIncl` 📖	CompOp	12 math math: `mapInclIsometry_apply`, `range_mapIncl`, `map₂_eq_range_lift_comp_mapIncl`, `LieModule.weight_vector_multiplication`, `inner_mapIncl_mapIncl`, `exists_finite_submodule_of_finite`, `Module.Flat.tensorProduct_mapIncl_injective_of_left`, `Submodule.mulMap_eq_mul'_comp_mapIncl`, `exists_finite_submodule_of_setFinite`, `Module.Flat.tensorProduct_mapIncl_injective_of_right`, `toLinearMap_mapInclIsometry`, `range_mapIncl_mono`
`map₂` 📖	CompOp	1 math math: `map₂_apply_tmul`
`rTensorHomToHomRTensor` 📖	CompOp	3 math math: `rTensorHomEquivHomRTensor_apply`, `rTensorHomEquivHomRTensor_toLinearMap`, `rTensorHomToHomRTensor_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_congr` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `TensorProduct` `addCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `congr` `LinearEquiv.trans`	—	`DFunLike.congr_fun` `congr_trans`
`congr_mul` 📖	mathematical	—	`congr` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHomInvPair.ids` `LinearEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `TensorProduct` `addCommMonoid` `instModule`	—	`RingHomInvPair.ids` `congr_trans`
`congr_pow` 📖	mathematical	—	`LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `addCommMonoid` `instModule` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `congr`	—	`RingHomInvPair.ids` `congr_refl_refl` `pow_succ` `congr_mul`
`congr_refl_refl` 📖	mathematical	—	`congr` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHomInvPair.ids` `LinearEquiv.refl` `TensorProduct` `addCommMonoid` `instModule`	—	`LinearEquiv.toLinearMap_injective` `RingHomInvPair.ids` `ext'`
`congr_symm` 📖	mathematical	—	`LinearEquiv.symm` `TensorProduct` `CommSemiring.toSemiring` `addCommMonoid` `instModule` `congr`	—	—
`congr_symm_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `TensorProduct` `addCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `congr` `tmul`	—	—
`congr_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `TensorProduct` `addCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `congr` `tmul`	—	—
`congr_trans` 📖	mathematical	—	`congr` `LinearEquiv.trans` `CommSemiring.toSemiring` `TensorProduct` `addCommMonoid` `instModule`	—	`LinearEquiv.toLinearMap_injective` `map_comp`
`congr_zpow` 📖	mathematical	—	`LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `addCommMonoid` `instModule` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `congr`	—	`RingHomInvPair.ids` `congr_pow` `zpow_negSucc` `congr_symm`
`homTensorHomMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `addCommMonoid` `instModule` `smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearMap.instFunLike` `homTensorHomMap` `tmul` `map`	—	`smulCommClass_self` `smulCommClass_left`
`instSmall` 📖	mathematical	—	`Small` `TensorProduct`	—	`RingHomInvPair.ids`
`lTensorHomToHomLTensor_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `TensorProduct` `addCommMonoid` `instModule` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `lTensorHomToHomLTensor` `tmul`	—	`smulCommClass_self` `smulCommClass_left`
`lift_comp_map` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `CommSemiring.toSemiring` `addCommMonoid` `instModule` `lift` `map` `LinearMap.compl₂` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module`	—	`smulCommClass_self` `ext'`
`mapBilinear_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `addCommMonoid` `instModule` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearMap.instFunLike` `LinearMap.instSMulCommClass` `DistribMulAction.toDistribSMul` `mapBilinear` `map`	—	`smulCommClass_self` `smulCommClass_left` `LinearMap.instSMulCommClass`
`map_add_left` 📖	mathematical	—	`map` `LinearMap` `CommSemiring.toSemiring` `LinearMap.instAdd` `TensorProduct` `addCommMonoid` `instModule`	—	`ext` `LinearMap.ext` `smulCommClass_self` `RingHomCompTriple.ids` `add_tmul`
`map_add_right` 📖	mathematical	—	`map` `LinearMap` `CommSemiring.toSemiring` `LinearMap.instAdd` `TensorProduct` `addCommMonoid` `instModule`	—	`ext` `LinearMap.ext` `smulCommClass_self` `RingHomCompTriple.ids` `tmul_add`
`map_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`TensorProduct` `addCommMonoid` `instModule` `map`	—	`LinearEquiv.bijective` `RingHomInvPair.ids`
`map_comm` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `TensorProduct` `addCommMonoid` `instModule` `LinearMap.instFunLike` `map` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `comm`	—	`DFunLike.congr_fun` `RingHomCompTriple.ids` `RingHomInvPair.ids` `RingHomCompTriple.right_ids` `map_comp_comm_eq`
`map_comp` 📖	mathematical	—	`map` `LinearMap.comp` `CommSemiring.toSemiring` `TensorProduct` `addCommMonoid` `instModule`	—	`ext'`
`map_comp_comm_eq` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `CommSemiring.toSemiring` `addCommMonoid` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `map` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `comm` `RingHomCompTriple.right_ids`	—	`ext` `RingHomCompTriple.ids` `RingHomInvPair.ids` `RingHomCompTriple.right_ids` `smulCommClass_self`
`map_id` 📖	mathematical	—	`map` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `LinearMap.id` `TensorProduct` `addCommMonoid` `instModule`	—	`ext` `LinearMap.ext` `smulCommClass_self` `RingHomCompTriple.ids`
`map_map` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `TensorProduct` `addCommMonoid` `instModule` `LinearMap.instFunLike` `map` `LinearMap.comp`	—	`DFunLike.congr_fun` `map_comp`
`map_mul` 📖	mathematical	—	`map` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `LinearMap` `Module.End.instMul` `TensorProduct` `addCommMonoid` `instModule`	—	`map_comp`
`map_one` 📖	mathematical	—	`map` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `LinearMap` `Module.End.instOne` `TensorProduct` `addCommMonoid` `instModule`	—	`map_id`
`map_pow` 📖	mathematical	—	`LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `addCommMonoid` `instModule` `Monoid.toNatPow` `Module.End.instMonoid` `map`	—	`pow_zero` `map_one` `pow_succ'` `map_mul`
`map_range_eq_span_tmul` 📖	mathematical	—	`LinearMap.range` `TensorProduct` `CommSemiring.toSemiring` `addCommMonoid` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `map` `Submodule.span` `setOf` `tmul` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	—	`range_map_eq_span_tmul`
`map_smul_left` 📖	mathematical	—	`map` `LinearMap` `CommSemiring.toSemiring` `LinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `TensorProduct` `addCommMonoid` `instModule` `instDistribMulAction` `smulCommClass_left`	—	`ext` `smulCommClass_self` `smulCommClass_left` `LinearMap.ext` `RingHomCompTriple.ids` `smul_tmul` `CompatibleSMul.isScalarTower` `IsScalarTower.left` `tmul_smul`
`map_smul_right` 📖	mathematical	—	`map` `LinearMap` `CommSemiring.toSemiring` `LinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `TensorProduct` `addCommMonoid` `instModule` `instDistribMulAction` `smulCommClass_left`	—	`ext` `smulCommClass_self` `smulCommClass_left` `LinearMap.ext` `RingHomCompTriple.ids` `tmul_smul` `CompatibleSMul.isScalarTower` `IsScalarTower.left`
`map_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `TensorProduct` `addCommMonoid` `instModule` `LinearMap.instFunLike` `map` `tmul`	—	—
`map_zero_left` 📖	mathematical	—	`map` `LinearMap` `CommSemiring.toSemiring` `LinearMap.instZero` `TensorProduct` `addCommMonoid` `instModule`	—	`LinearMap.map_zero₂` `smulCommClass_self` `smulCommClass_left` `LinearMap.instSMulCommClass`
`map_zero_right` 📖	mathematical	—	`map` `LinearMap` `CommSemiring.toSemiring` `LinearMap.instZero` `TensorProduct` `addCommMonoid` `instModule`	—	`LinearMap.map_zero` `smulCommClass_self` `smulCommClass_left` `LinearMap.instSMulCommClass`
`map₂_apply_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `TensorProduct` `addCommMonoid` `instModule` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `LinearMap.instFunLike` `map₂` `tmul` `map`	—	`smulCommClass_self` `smulCommClass_left`
`map₂_eq_range_lift_comp_mapIncl` 📖	mathematical	—	`Submodule.map₂` `LinearMap.range` `TensorProduct` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `addCommMonoid` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.comp` `RingHomCompTriple.ids` `lift` `mapIncl`	—	`smulCommClass_self` `RingHomSurjective.ids` `RingHomCompTriple.ids` `LinearMap.range_comp` `Submodule.map.congr_simp` `range_mapIncl` `IsScalarTower.left` `Submodule.map_map₂`
`rTensorHomToHomRTensor_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `TensorProduct` `addCommMonoid` `instModule` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `rTensorHomToHomRTensor` `tmul`	—	`smulCommClass_self` `smulCommClass_left`
`range_map` 📖	mathematical	—	`LinearMap.range` `TensorProduct` `CommSemiring.toSemiring` `addCommMonoid` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `map` `Submodule.map₂`	—	`RingHomSurjective.ids` `smulCommClass_self` `Submodule.map₂_map_map` `Submodule.map.congr_simp` `IsScalarTower.left` `Submodule.map_map₂`
`range_mapIncl` 📖	mathematical	—	`LinearMap.range` `TensorProduct` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `addCommMonoid` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `mapIncl` `Submodule.map₂`	—	`RingHomSurjective.ids` `range_map` `Submodule.range_subtype`
`range_mapIncl_mono` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	`TensorProduct` `addCommMonoid` `instModule` `LinearMap.range` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `mapIncl`	—	`range_map_mono` `RingHomSurjective.ids` `Submodule.range_subtype`
`range_map_eq_span_tmul` 📖	mathematical	—	`LinearMap.range` `TensorProduct` `CommSemiring.toSemiring` `addCommMonoid` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `map` `Submodule.span` `setOf` `tmul` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	—	`RingHomSurjective.ids` `Submodule.map.congr_simp` `Submodule.map_span` `Set.ext`
`range_map_mono` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids`	`TensorProduct` `addCommMonoid` `instModule` `map`	—	`RingHomSurjective.ids` `range_map` `Submodule.map₂_le_map₂`
`toLinearMap_congr` 📖	mathematical	—	`LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `TensorProduct` `addCommMonoid` `instModule` `congr` `map`	—	—

---

← Back to Index