Documentation Verification Report

TensorProduct

📁 Source: Mathlib/RingTheory/Spectrum/Prime/TensorProduct.lean

Statistics

Metric	Count
Definitions `tensorProductTo`, `TensorProduct`	2
Theorems `continuous_tensorProductTo`, `isEmbedding_tensorProductTo_of_surjectiveOnStalks`, `isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux`	3
Total	5

PrimeSpectrum

Definitions

Name	Category	Theorems
`tensorProductTo` 📖	CompOp	2 math math: `isEmbedding_tensorProductTo_of_surjectiveOnStalks`, `continuous_tensorProductTo`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_tensorProductTo` 📖	mathematical	—	`Continuous` `PrimeSpectrum` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instCommSemiring` `zariskiTopology` `instTopologicalSpaceProd` `tensorProductTo`	—	`Continuous.prodMk` `continuous_comap`
`isEmbedding_tensorProductTo_of_surjectiveOnStalks` 📖	mathematical	`RingHom.SurjectiveOnStalks` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`Topology.IsEmbedding` `PrimeSpectrum` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Algebra.TensorProduct.instCommSemiring` `zariskiTopology` `instTopologicalSpaceProd` `tensorProductTo`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `LE.le.antisymm` `Continuous.le_induced` `continuous_tensorProductTo` `TopologicalSpace.Opens.IsBasis.le_iff` `isBasis_basic_opens` `isOpen_iff_forall_mem_open` `RingHom.instRingHomClass` `RingHom.SurjectiveOnStalks.exists_mul_eq_tmul` `Ideal.IsPrime.comap` `isPrime` `Submonoid.mul_mem` `Algebra.TensorProduct.tmul_mul_tmul` `mul_one` `one_mul` `Ideal.mul_mem_left` `IsOpen.prod` `TopologicalSpace.Opens.is_open'` `Iff.not` `Ideal.IsPrime.mul_mem_iff_mem_or_mem` `Ideal.instIsTwoSided_1` `isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux`
`isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux` 📖	mathematical	`RingHom.SurjectiveOnStalks` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `tensorProductTo`	`PrimeSpectrum` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Algebra.TensorProduct.instCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `RingHom.instRingHomClass` `RingHom.SurjectiveOnStalks.exists_mul_eq_tmul` `Ideal.IsPrime.comap` `isPrime` `Ideal.mul_mem_left` `Submonoid.mul_mem` `Algebra.TensorProduct.tmul_mul_tmul` `one_mul` `mul_one` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1`

(root)

Definitions

Name	Category	Theorems
`TensorProduct` 📖	CompOp	1804 math math: `CommRingCat.tensorProd_map_right`, `Pi.comul_eq_adjoint`, `TensorProduct.finsuppRight_apply`, `DFinsupp.comul_single`, `SemimoduleCat.MonoidalCategory.triangle`, `TensorProduct.mapInclIsometry_apply`, `LinearMap.lTensor_ker_subtype_tensorKerEquiv_symm`, `Algebra.TensorProduct.congr_trans`, `KaehlerDifferential.kerCotangentToTensor_toCotangent`, `Representation.repOfTprodIso_inv_apply`, `exists_fg_and_mem_baseChange`, `CliffordAlgebra.toBaseChange_reverse`, `Algebra.FormallyUnramified.one_tmul_mul_elem`, `TensorProduct.congr_symm`, `Subalgebra.mulMap_comm`, `Bialgebra.comulAlgHom_apply`, `TensorProduct.forall_vanishesTrivially_iff_forall_fg_rTensor_injective`, `Submodule.rTensorOne_symm_apply`, `Bialgebra.comul_natCast`, `lTensor.inverse_comp_lTensor`, `LinearMap.baseChange_eq_ltensor`, `Module.Flat.iff_lTensor_exact'`, `TensorProduct.enorm_lid`, `Algebra.Generators.baseChange_val`, `Submodule.FG.rTensor.directedSystem`, `Ideal.comap_fiberIsoOfBijectiveResidueField_apply`, `TensorProduct.inner_tmul`, `Matrix.toLin_kronecker`, `AlternatingMap.domCoprod.summand_mk''`, `Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_right`, `TensorProduct.LieModule.liftLie_apply`, `Algebra.TensorProduct.instSMulCommClassTensorProduct`, `Algebra.TensorProduct.lift_comp_includeLeft`, `Coalgebra.lTensor_counit_comul`, `Matrix.kroneckerTMulStarAlgEquiv_symm_apply`, `RingHom.SurjectiveOnStalks.baseChange`, `LinearEquiv.lTensor_pow`, `TensorProduct.ext_iff_inner_left`, `Rep.MonoidalClosed.linearHomEquiv_symm_hom`, `Algebra.TensorProduct.intCast_def'`, `GradedTensorProduct.hom_ext_iff`, `Module.Basis.tensorProduct_apply`, `TensorProduct.AlgebraTensorModule.rid_symm_apply`, `Algebra.TensorProduct.prodRight_tmul_fst`, `Module.FaithfullyFlat.iff_exact_iff_lTensor_exact`, `IsGroupLikeElem.comul_eq_tmul_self`, `MvPolynomial.rTensor_apply_tmul_apply`, `PrimeSpectrum.preimageEquivFiber_symm_apply_coe`, `PiTensorProduct.tmulEquiv_symm_apply`, `TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm`, `LinearMap.baseChange_smul`, `MvPolynomial.rTensorAlgEquiv_apply`, `Algebra.Generators.H1Cotangent.δAux_mul`, `AlgCat.hom_inv_associator`, `LinearMap.convMul_def`, `BialgCat.rightUnitor_def`, `HopfAlgCat.rightUnitor_def`, `Submodule.mulMap_tmul`, `Algebra.TensorProduct.includeLeft_map_center_le`, `Submodule.comm_trans_lTensorOne`, `MvPolynomial.scalarRTensor_apply_monomial_tmul`, `LieSubmodule.lowerCentralSeries_tensor_eq_baseChange`, `LinearMap.lTensor_sub`, `LaurentPolynomial.comul_T`, `Submodule.exists_fg_le_eq_rTensor_inclusion`, `finsuppTensorFinsupp_apply`, `MvPolynomial.universalFactorizationMap_comp_map`, `TensorProduct.range_mapIncl`, `CommRingCat.pushoutCocone_pt`, `TensorProduct.congr_congr`, `Representation.repOfTprodIso_apply`, `TensorProduct.instSmall`, `LinearMap.rTensor_comm`, `LinearMap.BilinMap.baseChange_isSymm`, `TensorProduct.equivFinsuppOfBasisLeft_symm_apply`, `Subalgebra.LinearDisjoint.include_range`, `Submodule.tensorEquivSpan_apply_tmul`, `LinearMap.baseChange_comp`, `LinearEquiv.coe_baseChange`, `KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul'`, `CommAlgCat.braiding_hom_hom`, `TensorProduct.AlgebraTensorModule.congr_refl`, `TensorProduct.smul_add`, `Module.FaithfullyFlat.lTensor_injective_iff_injective`, `kroneckerTMulAlgEquiv_symm_single_tmul`, `Rep.coindToInd_of_support_subset_orbit`, `Module.Flat.iff_rTensor_preserves_injective_linearMap`, `Algebra.IsPushout.equiv_symm_algebraMap_left`, `Bialgebra.TensorProduct.map_toAlgHom`, `AddMonoidAlgebra.comul_single`, `Algebra.IsIntegral.tensorProduct`, `Representation.Coinvariants.mk_inv_tmul`, `LinearMap.tensorKer_tmul`, `TensorProduct.AlgebraTensorModule.map_id`, `LinearMap.lTensor_rTensor_comp_assoc`, `Module.rankAtStalk_eq`, `TensorProduct.sum_tmul_basis_right_injective`, `Algebra.TensorProduct.congr_symm_apply`, `Pi.comul_comp_dFinsuppCoeFnLinearMap`, `Submodule.mulMap_one_right_eq`, `TensorProduct.star_tmul`, `PolynomialLaw.factorsThrough_toFunLifted_π`, `TensorProduct.toIntegralClosure_bijective_of_isLocalization`, `TensorProduct.piScalarRight_symm_algebraMap`, `OrthonormalBasis.toBasis_tensorProduct`, `TensorProduct.congrIsometry_refl_refl`, `Algebra.TensorProduct.mapOfCompatibleSMul_surjective`, `TensorProduct.AlgebraTensorModule.congr_symm`, `TensorProduct.enorm_comm`, `Algebra.TensorProduct.natCast_def'`, `LinearMap.rTensor_smul_action`, `TensorProduct.AlgebraTensorModule.rid_tmul`, `KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul`, `Coalgebra.sum_map_tmul_counit_eq`, `Algebra.IsPushout.cancelBaseChange_tmul`, `TensorProduct.span_tmul_eq_top`, `TensorProduct.tensorTensorTensorComm_tmul`, `PolyEquivTensor.right_inv`, `TensorProduct.gradedComm_tmul_one`, `TensorProduct.AlgebraTensorModule.congr_symm_tmul`, `Coalgebra.sum_tmul_counit_eq`, `Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single`, `Algebra.FormallyUnramified.lmul_elem`, `QuotSMulTop.equivTensorQuot_naturality`, `MonoidAlgebra.tensorEquiv.invFun_tmul`, `Module.Flat.lTensor_preserves_injective_linearMap`, `Module.Flat.ker_lTensor_eq`, `KaehlerDifferential.cotangentComplexBaseChange_tmul`, `TensorProduct.tensorTensorTensorComm_comp_map`, `Module.Invertible.instTensorProduct_1`, `TensorProduct.range_map`, `AlgebraicGeometry.diagonal_SpecMap`, `CoalgCat.MonoidalCategoryAux.associator_hom_toLinearMap`, `Matrix.kroneckerTMul_zero`, `Coalgebra.coassoc_symm_apply`, `LinearMap.tensorEqLocusEquiv_apply`, `Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul`, `lTensor.inverse_of_rightInverse_comp_lTensor`, `LinearMap.baseChange_baseChange`, `Algebra.TensorProduct.prodRight_symm_tmul`, `Algebra.TensorProduct.tensorTensorTensorComm_symm`, `IsLocalization.mk'_tmul`, `TensorPower.gMul_eq_coe_linearMap`, `IsSMulRegular.lTensor`, `TensorProduct.map_injective_of_flat_flat_of_isDomain`, `LinearMap.lTensor_id_apply`, `TensorProduct.map_comp_comm_eq`, `InnerProductSpace.canonicalCovariantTensor_eq_sum`, `Module.Flat.lTensor_exact`, `Module.FaithfullyFlat.lTensor_exact_iff_exact`, `Algebra.TensorProduct.map_comp`, `AlgCat.hom_inv_rightUnitor`, `AlternatingMap.domCoprod_coe`, `AdicCompletion.ofTensorProduct_surjective_of_finite`, `MvPolynomial.scalarRTensor_apply_X_tmul_apply`, `TensorProduct.ext_iff_inner_right_threefold'`, `TensorProduct.map_add_right`, `Module.FaithfullyFlat.lTensor_bijective_iff_bijective`, `Algebra.FormallyUnramified.finite_of_free_aux`, `rTensor_injective_iff_lcomp_surjective`, `TensorProduct.gradedMul_assoc`, `Subalgebra.centralizer_coe_map_includeLeft_eq_center_tensorProduct`, `TensorProduct.toLinearEquiv_lidIsometry`, `contractLeft_assoc_coevaluation`, `Matrix.kroneckerTMul_assoc'`, `Bialgebra.TensorProduct.counitAlgHom_def`, `Algebra.TensorProduct.algebraMap_apply`, `Submodule.FG.lTensor.directedSystem`, `LinearMap.rTensor_id`, `CommRing.Pic.mul_eq_tensor`, `TensorProduct.AlgebraTensorModule.rightComm_symm_tmul`, `LinearMap.tensorKer_coe`, `Module.rank_baseChange`, `TensorProduct.map_map`, `Algebra.PreSubmersivePresentation.baseChange_jacobian`, `Algebra.IsPushout.cancelBaseChange_symm_tmul`, `IsLocalization.instIsLocalizedModuleTensorProductMap`, `Algebra.TensorProduct.piRightHom_mul`, `Submodule.val_mulMap'_tmul`, `TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor`, `CliffordAlgebra.equivBaseChange_symm_apply`, `LinearMap.lTensor_smul`, `Module.FaithfullyFlat.instTensorProduct`, `TensorProduct.directSum_lof_tmul_lof`, `KaehlerDifferential.kerToTensor_apply`, `TensorProduct.AlgebraTensorModule.lTensor_comp_cancelBaseChange`, `instIsLocalRingTensorProductResidueFieldOfIsLocalHomRingHomAlgebraMap`, `TensorProduct.AlgebraTensorModule.lTensor_id`, `RingHom.SurjectiveOnStalks.exists_mul_eq_tmul`, `TensorProduct.isScalarTower_right`, `TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul`, `Pi.comul_comp_single`, `zero_prodMap_dualTensorHom`, `LinearMap.mul'_comp_comm`, `TensorProduct.AlgebraTensorModule.rTensor_one`, `Algebra.TensorProduct.basis_apply`, `LinearMap.lTensor_surj_iff_rTensor_surj`, `LinearMap.liftBaseChange_one_tmul`, `TensorProduct.zero_smul`, `Subalgebra.mulMap_toLinearMap`, `Algebra.TensorProduct.piScalarRight_tmul`, `LinearMap.rTensor_id_apply`, `KaehlerDifferential.isScalarTower'`, `AlgHom.mulLeftRightMatrix.inv_comp`, `LinearEquiv.rTensor_mul`, `le_comap_range_lTensor`, `BialgCat.associator_def`, `TensorProduct.liftAux_tmul`, `QuotSMulTop.equivTensorQuot_naturality_mk`, `Module.endTensorEndAlgHom_apply`, `tensorIteratedFDerivTwo_eq_iteratedFDeriv`, `TensorProduct.coe_directSumRight'`, `Algebra.TensorProduct.comm_comp_map_apply`, `finsuppTensorFinsupp'_symm_single_eq_tmul_single_one`, `Rep.finsuppToCoinvariantsTensorFree_single`, `PolyEquivTensor.toFunAlgHom_apply_tmul`, `PolynomialLaw.exists_lift'`, `LinearMap.toMatrix_baseChange`, `TensorProduct.nontrivial_of_linearMap_injective_of_flat_right`, `BialgCat.whiskerLeft_def`, `Coalgebra.sum_counit_tmul_eq`, `HopfAlgCat.whiskerLeft_def`, `SemimoduleCat.hom_inv_rightUnitor`, `TensorProduct.adjoint_map`, `LinearIsometryEquiv.lTensor_apply`, `TensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse`, `LinearMap.rTensor_comp_lTensor`, `Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange`, `LinearMap.rTensor_comp_map`, `LinearMap.rTensor_comp_flip_mk`, `Algebra.TensorProduct.sMulCommClass_right`, `TensorProduct.dualDistrib_apply_comm`, `Representation.Coinvariants.mk_tmul_inv`, `CharacterModule.curry_apply_apply`, `Algebra.IsStandardSmoothOfRelativeDimension.baseChange`, `LinearEquiv.coe_lTensor`, `IsPurelyInseparable.exists_pow_mem_range_tensorProduct`, `Algebra.TensorProduct.assoc_tmul`, `Algebra.IsAlgebraic.tensorProduct`, `TensorProduct.map₂_eq_range_lift_comp_mapIncl`, `Subalgebra.comm_trans_rTensorBot`, `Module.FaithfullyFlat.iff_zero_iff_rTensor_zero`, `Subalgebra.mulMap_map_comp_eq`, `TensorProduct.directLimitRight_tmul_of`, `TensorProduct.mapIsometry_id_id`, `KaehlerDifferential.ideal_fg`, `Algebra.TensorProduct.map_tmul`, `TensorProduct.flip_mk_surjective`, `LinearMap.rTensor_tmul`, `TensorProduct.exists_finite_submodule_of_finite'`, `TensorProduct.toIntegralClosure_bijective_of_smooth`, `TensorProduct.tensorQuotEquivQuotSMul_comp_mkQ_lTensor`, `Algebra.instIsReducedTensorProductOfIsAlgebraicOfIsGeometricallyReduced`, `Algebra.isGeometricallyReduced_iff`, `Algebra.Generators.liftBaseChange_injective_of_isLocalizationAway`, `TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply`, `CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_right`, `TensorProduct.leftComm_tmul`, `Orthonormal.basisTensorProduct`, `TensorProduct.comm_comm`, `LinearMap.det_baseChange`, `QuadraticForm.tmul_tensorMap_apply`, `Submodule.mulMap_comm`, `Algebra.TensorProduct.algEquivIncludeRange_symm_tmul`, `Module.Flat.out`, `TensorProduct.map_injective_of_flat_flat'`, `TensorProduct.AlgebraTensorModule.map_smul_left`, `Algebra.TensorProduct.leftComm_tmul`, `LinearEquiv.det_baseChange`, `TensorProduct.gradedMul_def`, `rTensor.inverse_of_rightInverse_apply`, `Algebra.TensorProduct.includeRight_apply`, `KaehlerDifferential.instIsScalarTowerTensorProduct`, `CommRingCat.pushoutCocone_inl`, `ModuleCat.MonoidalCategory.associator_hom_apply`, `TensorProduct.AlgebraTensorModule.restrictScalars_lTensor`, `Finsupp.linearCombination_one_tmul`, `Module.FaithfullyFlat.lTensor_surjective_iff_surjective`, `CliffordAlgebra.ofBaseChange_toBaseChange`, `TensorProduct.AlgebraTensorModule.restrictScalars_curry`, `LinearMap.trace_eq_contract_of_basis'`, `Submodule.linearDisjoint_iff`, `QuadraticForm.tmul_comp_tensorComm`, `QuadraticForm.polarBilin_baseChange`, `PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal`, `LinearEquiv.comm_trans_lTensor_trans_comm_eq`, `GradedTensorProduct.auxEquiv_one`, `Algebra.TensorProduct.basis_repr_tmul`, `CoalgHom.map_comp_comul`, `TensorProduct.toMatrix_assoc`, `Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap`, `Module.FaithfullyFlat.zero_iff_rTensor_zero`, `LinearMap.lTensor_comp_comm`, `Polynomial.X_pow_smul_rTensor_monomial`, `Algebra.TensorProduct.linearEquivIncludeRange_toLinearMap`, `retractionOfSectionOfKerSqZero_comp_kerToTensor`, `LinearMap.coe_lTensorHom`, `KaehlerDifferential.mapBaseChange_tmul`, `MatrixEquivTensor.invFun_add`, `ModuleCat.ExtendRestrictScalarsAdj.Counit.map_hom_apply`, `LinearMap.baseChange_one`, `PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks`, `TensorProduct.tmul_sub`, `Matrix.toAlgEquiv_kroneckerStarAlgEquiv`, `Bialgebra.TensorProduct.map_toCoalgHom`, `Algebra.Generators.H1Cotangent.δAux_C`, `TensorProduct.gradedComm_algebraMap_tmul`, `LinearMap.BilinMap.tmul_isSymm`, `TensorProduct.finsuppLeft_smul'`, `Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField`, `CliffordAlgebra.toBaseChange_comp_ofBaseChange`, `PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal`, `TensorProduct.liftAddHom_tmul`, `Coalgebra.sum_map_tmul_tmul_eq`, `Algebra.TensorProduct.basisAux_map_smul`, `PolynomialLaw.smul_def`, `Pi.intrinsicStar_comul_commSemiring`, `TensorProduct.equivFinsuppOfBasisRight_apply_tmul`, `TensorProduct.congr_zpow`, `ModuleCat.MonoidalCategory.whiskerLeft_def`, `LinearMap.lTensor_range`, `Coalgebra.comm_comul`, `LocalizedModule.equivTensorProduct_symm_apply_tmul_one`, `Rep.ihom_ev_app_hom`, `CommRing.Pic.mk_tensor`, `LocalizedModule.equivTensorProduct_apply_mk`, `Algebra.TensorProduct.lid_tmul`, `CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc`, `Module.Flat.iff_lTensor_preserves_injective_linearMap`, `lTensor.inverse_of_rightInverse_apply`, `TensorProduct.equivFinsuppOfBasisLeft_apply_tmul`, `QuadraticForm.polarBilin_tmul`, `TensorProduct.lidIsometry_apply`, `Module.Presentation.tensor_R`, `LinearEquiv.lTensor_zpow`, `Module.FaithfullyFlat.lTensor_nontrivial`, `Matrix.toAlgEquiv_kroneckerTMulStarAlgEquiv`, `Algebra.TensorProduct.tensorTensorTensorComm_symm_tmul`, `isGroupLikeElem_iff`, `LinearMap.tensorKerEquivOfSurjective_symm_tmul`, `TensorProduct.equivFinsuppOfBasisLeft_symm`, `KaehlerDifferential.mulActionBaseChange_smul_add`, `TensorProduct.comm_trans_lid`, `TensorProduct.Algebra.smul_def`, `Module.FaithfullyFlat.subsingleton_tensorProduct_iff_right`, `LinearMap.tensorEqLocus_coe`, `tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin`, `PointedCone.tmul_mem_maxTensorProduct`, `TensorProduct.curry_injective`, `Algebra.TensorProduct.includeLeft_apply`, `lTensorHomEquivHomLTensor_apply`, `TensorProduct.finsuppScalarRight_apply`, `Algebra.FormallySmooth.iff_injective_lTensor_residueField`, `Ideal.Fiber.lift_residueField_surjective`, `Module.FaithfullyFlat.nontrivial_tensorProduct_iff_right`, `isBaseChange_tensorProduct_map`, `LinearMap.trace_eq_contract`, `LinearEquiv.rTensor_trans_congr`, `LocalizedModule.equivTensorProduct_symm_apply_tmul`, `LinearMap.rTensor_sub`, `Module.comap_freeLocus_le`, `CliffordAlgebra.toBaseChange_comp_involute`, `TensorProduct.finsuppScalarRight_apply_tmul`, `TensorProduct.rightComm_symm`, `Algebra.IsEpi.injective_lift_mul`, `Algebra.TensorProduct.right_algebraMap_apply`, `Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap`, `Coalgebra.TensorProduct.lid_tmul`, `homTensorHomEquiv_apply`, `TensorProduct.mk_apply`, `TensorProduct.mapOfCompatibleSMul_surjective`, `Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop_symm_apply`, `finsuppTensorFinsupp'_single_tmul_single`, `TensorProduct.smul_zero`, `Module.Flat.iff_rTensor_injective`, `ModuleCat.MonoidalCategory.tensorHom_def`, `LinearMap.baseChange_pow`, `Representation.tprod_apply`, `CommRingCat.pushoutCocone_inr`, `dualTensorHom_apply`, `TensorProduct.Algebra.exists_of_fg`, `QuadraticForm.tensorRId_symm_apply`, `Module.Invertible.tensorProductComm_eq_refl`, `LinearEquiv.lTensor_trans_congr`, `Module.Invertible.rTensorEquiv_apply_apply`, `lTensorHomEquivHomLTensor_toLinearMap`, `LinearEquiv.lTensor_tmul`, `Ideal.map_includeRight_eq`, `Algebra.TensorProduct.includeLeft_bijective`, `AlgebraicGeometry.pullbackSpecIso_inv_snd`, `AlgHom.comp_mul'`, `Subalgebra.centralizer_coe_image_includeRight_eq_center_tensorProduct`, `LinearMap.intrinsicStar_mul'`, `TensorProduct.exists_finite_submodule_left_of_setFinite`, `TensorProduct.quotientTensorEquiv_symm_apply_mk_tmul`, `AlgCat.hom_hom_associator`, `LinearEquiv.rTensor_zpow`, `MonoidAlgebra.scalarTensorEquiv_tmul`, `QuadraticForm.tensorAssoc_toLinearEquiv`, `TensorProduct.AlgebraTensorModule.rTensor_tensor`, `TensorProduct.neg_tmul`, `Algebra.PreSubmersivePresentation.baseChange_toPresentation`, `LinearMap.polyCharpoly_baseChange`, `TensorProduct.AlgebraTensorModule.rTensor_comp`, `coevaluation_apply_one`, `LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul`, `IsLocalRing.map_tensorProduct_mk_eq_top`, `Bialgebra.TensorProduct.comulAlgHom_def`, `Representation.coinvariantsTprodLeftRegularLEquiv_apply`, `finsuppTensorFinsuppLid_symm_single_smul`, `LinearMap.lTensor_surjective`, `TensorProduct.congr_refl_refl`, `rTensorHomEquivHomRTensor_apply`, `LinearMap.trace_eq_contract_apply`, `TensorProduct.congr_trans`, `dualTensorHomEquivOfBasis_symm_cancel_right`, `TensorProduct.tmul_smul`, `SemiconjBy.tmul`, `TensorProduct.map_add_left`, `MvPolynomial.scalarRTensor_apply_tmul`, `TensorProduct.prodLeft_tmul`, `PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field`, `TensorProduct.tensorTensorTensorComm_symm`, `IsLocalization.tensorProduct_isLocalizedModule`, `MultilinearMap.domCoprodDep_apply`, `Algebra.TensorProduct.map_ker`, `AddMonoidAlgebra.tensorEquiv.invFun_tmul`, `finsuppTensorFinsupp'_symm_single_mul`, `Algebra.TensorProduct.includeRight_map_center_le`, `Algebra.TensorProduct.productMap_left_apply`, `Algebra.TensorProduct.instSMulCommClassTensorProduct_1`, `Algebra.TensorProduct.algebraMap_eq_includeRight`, `CoalgCat.tensorHom_def`, `Submodule.surjective_tensorToSpan`, `CommRingCat.coproductCocone_inl`, `LinearMap.BilinForm.tensorDistribEquiv_toLinearMap`, `Subalgebra.lTensorBot_one_tmul`, `PolyEquivTensor.toFunLinear_mul_tmul_mul`, `TensorProduct.directSumRight_comp_rTensor`, `SemimoduleCat.hom_hom_rightUnitor`, `KaehlerDifferential.tensorKaehlerEquivBase_tmul`, `lTensor.inverse_apply`, `AlgebraicGeometry.pullbackSpecIso_hom_base`, `TensorProduct.map_map_assoc_symm`, `Module.Invertible.bijective_curry`, `KaehlerDifferential.tensorKaehlerEquivBase_symm_apply`, `Algebra.TensorProduct.productMap_left`, `Subalgebra.mulMap_bot_left_eq`, `TensorProduct.comm_symm`, `TensorProduct.instDirectedSystemCoeLinearMapIdRTensor`, `Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap`, `GradedTensorProduct.auxEquiv_symm_one`, `LinearMap.adjoint_rTensor`, `GradedTensorProduct.auxEquiv_comm`, `TensorProduct.finsuppLeft_symm_apply_single`, `Algebra.TensorProduct.productMap_apply_tmul`, `LinearMap.rTensor_injective_iff_subtype`, `LinearMap.BilinForm.tensorDistrib_tmul`, `TensorProduct.AlgebraTensorModule.mk_apply`, `QuadraticForm.baseChange_tmul`, `PolynomialLaw.toFun_add_apply`, `KaehlerDifferential.End_equiv_aux`, `IsTensorProduct.equiv_symm_apply`, `TensorProduct.ext_iff_inner_left_threefold'`, `RingTheory.Sequence.IsWeaklyRegular.isWeaklyRegular_lTensor`, `LinearIsometry.lTensor_apply`, `finsuppTensorFinsupp'_apply_apply`, `Algebra.IsGeometricallyReduced.isReduced_algebraicClosure_tensorProduct`, `LinearMap.mul'_apply`, `Rep.coinvariantsTensorFreeLEquiv_apply`, `AlgHom.coe_tensorEqualizer`, `TensorProduct.toIntegralClosure_mvPolynomial_bijective`, `TensorProduct.AlgebraTensorModule.rTensor_tmul`, `TensorProduct.prodLeft_symm_tmul`, `TensorProduct.ext_iff_inner_left_threefold`, `Module.FaithfullyFlat.rTensor_exact_iff_exact`, `Module.rankAtStalk_baseChange`, `KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_apply`, `LinearEquiv.rTensor_refl_apply`, `Algebra.TensorProduct.lmul'_apply_tmul`, `MultilinearMap.domCoprod_alternization_coe`, `TensorProduct.inner_lid_lid`, `TensorProduct.tmul_eq_smul_one_tmul`, `LinearMap.BilinForm.tensorDistribEquiv_apply`, `Algebra.Generators.H1Cotangent.exact_map_δ`, `Algebra.Generators.H1Cotangent.δAux_monomial`, `TensorProduct.norm_comm`, `TensorProduct.map₂_apply_tmul`, `PrimeSpectrum.preimageEquivFiber_apply_asIdeal`, `Algebra.TensorProduct.includeLeft_injective`, `Algebra.Generators.CotangentSpace.compEquiv_symm_zero`, `TensorProduct.dualDistribEquivOfBasis_symm_apply`, `LieModule.weight_vector_multiplication`, `TensorProduct.leftComm_def`, `OrthonormalBasis.tensorProduct_repr_tmul_apply'`, `LinearMap.rTensor_lTensor_comp_assoc_symm`, `RingHom.SurjectiveOnStalks.tensorProductMap`, `HopfAlgCat.whiskerRight_def`, `LinearMap.liftBaseChangeEquiv_symm_apply`, `Finsupp.comul_comp_lapply`, `Algebra.TensorProduct.equivFinsuppOfBasis_apply`, `Matrix.smul_kroneckerTMul`, `PrimeSpectrum.mem_image_comap_basicOpen`, `CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_left`, `TensorProduct.gradedComm_algebraMap`, `TensorProduct.map_map_comp_assoc_eq`, `CommRingCat.isPushout_tensorProduct`, `Algebra.TensorProduct.opAlgEquiv_apply`, `CoalgCat.associator_def`, `PolynomialLaw.π_surjective`, `LinearMap.BilinForm.IsSymm.baseChange`, `TensorProduct.norm_assoc`, `TensorProduct.nnnorm_tmul`, `TensorProduct.lift.tmul'`, `TensorProduct.assoc_tmul`, `Algebra.TensorProduct.equivFinsuppOfBasis_symm_apply`, `QuadraticForm.tensorRId_apply`, `MvPolynomial.rTensor_apply_X_tmul`, `QuadraticForm.comp_tensorLId_eq`, `Algebra.FiniteType.baseChangeAux_surj`, `TensorProduct.LinearIndepOn.tmul_of_flat_right`, `KaehlerDifferential.exact_mapBaseChange_map`, `CommAlgCat.binaryCofan_pt`, `LinearMap.tensorProductEnd_apply`, `ModuleCat.hom_inv_associator`, `Bialgebra.TensorProduct.assoc_tmul`, `KaehlerDifferential.tensorKaehlerEquiv_tmul`, `TensorProduct.inner_mapIncl_mapIncl`, `LinearMap.trace_eq_contract'`, `Algebra.Generators.H1Cotangent.δAux_toAlgHom`, `Matrix.kroneckerAlgEquiv_apply`, `KaehlerDifferential.D_apply`, `InnerProductSpace.AlgebraOfCoalgebra.mul_def`, `TensorProduct.exists_finite_submodule_right_of_setFinite`, `lTensor_exact`, `TensorProduct.AlgebraTensorModule.leftComm_tmul`, `TensorProduct.tmul_zero`, `LieAlgebra.instIsSolvableTensorProduct`, `CoalgCat.MonoidalCategoryAux.tensorObj_comul`, `TensorProduct.gradedComm_tmul_of_zero`, `CoalgCat.comul_def`, `TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply`, `IsLocalization.Away.tensorRight`, `Module.End.rTensorAlgHom_apply_apply`, `Module.Flat.iff_lTensor_exact`, `PolynomialLaw.exists_lift`, `ModuleCat.MonoidalCategory.rightUnitor_def`, `CommRingCat.coproductCocone_inr`, `CommRing.Pic.mapAlgebra_apply`, `polyEquivTensor_symm_apply_tmul`, `AlgebraicGeometry.pullbackSpecIso_inv_fst'_assoc`, `KaehlerDifferential.one_smul_sub_smul_one_mem_ideal`, `TensorProduct.congr_tmul`, `IsAzumaya.mulLeftRight_comp_congr`, `Algebra.TensorProduct.algebraMap_def`, `MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval`, `MvPolynomial.finitePresentation_universalFactorizationMap`, `HopfAlgCat.associator_def`, `Module.Flat.rTensor_exact`, `KaehlerDifferential.range_mapBaseChange`, `Algebra.TensorProduct.includeRight_injective`, `Algebra.TensorProduct.isScalarTower_right`, `ModuleCat.MonoidalCategory.associator_def`, `MvPolynomial.tensorEquivSum_one_tmul_C`, `MultilinearMap.domCoprod_domDomCongr_sumCongr`, `LinearEquiv.rTensor_pow`, `Ideal.pi_tensorProductMk_quotient_surjective`, `TensorProduct.instStarModule`, `MvPolynomial.rTensor_apply_tmul`, `TensorProduct.AlgebraTensorModule.congr_mul`, `TensorProduct.nnnorm_map`, `Module.FaithfullyFlat.iff_exact_iff_rTensor_exact`, `AlgHom.mulLeftRight_apply`, `Algebra.TensorProduct.commRight_tmul`, `Module.Flat.iff_lTensor_preserves_injective_linearMap'`, `LinearMap.lTensor_smul_action`, `transpose_dualTensorHom`, `TensorProduct.AlgebraTensorModule.assoc_tmul`, `Rep.indResAdjunction_counit_app_hom_hom`, `LinearMap.lTensor_neg`, `Submodule.coe_tensorSpanEquivSpan_apply_tmul`, `Algebra.TensorProduct.lmul'_comp_map`, `LieSubmodule.mem_baseChange_iff`, `LinearEquiv.baseChange_mul`, `QuadraticMap.associated_tmul`, `Submodule.FG.lTensor.directLimit_apply'`, `IsAzumaya.bij`, `TensorProduct.directSumLeft_tmul_lof`, `Algebra.QuasiFinite.baseChange`, `Algebra.Generators.H1Cotangent.exact_δ_map`, `Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_comp_inl`, `Rep.coindToInd_apply`, `kroneckerTMulLinearEquiv_one`, `MultilinearMap.domCoprod_alternization_eq`, `TensorProduct.AlgebraTensorModule.leftComm_symm_tmul`, `Algebra.TensorProduct.lift_comp_includeRight`, `TensorProduct.AlgebraTensorModule.rightComm_tmul`, `KaehlerDifferential.mapBaseChange_surjective`, `ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply`, `Module.FaithfullyFlat.iff_zero_iff_lTensor_zero`, `AdicCompletion.coe_ofTensorProductEquivOfFiniteNoetherian`, `PolynomialLaw.toFun_zero`, `TensorProduct.AlgebraTensorModule.assoc_symm_tmul`, `TensorProduct.algebraMap_gradedMul`, `Subalgebra.centralizer_coe_map_includeRight_eq_center_tensorProduct`, `MonoidAlgebra.tensorEquiv_symm_single`, `Submodule.FG.rTensor.directLimit_apply`, `TensorProduct.directLimitLeft_rTensor_of`, `TensorProduct.finsuppScalarRight_smul`, `LinearMap.toMvPolynomial_baseChange`, `CoalgCat.whiskerRight_def`, `Algebra.TensorProduct.map_id`, `TensorProduct.lid_symm_apply`, `IsTensorProduct.equiv_apply`, `Bialgebra.comul_algebraMap`, `TensorProduct.lift_compr₂ₛₗ`, `TensorProduct.tensorQuotEquivQuotSMul_tmul_mk`, `AlgCat.hom_hom_rightUnitor`, `finsuppTensorFinsupp_single`, `TensorProduct.counit_tmul`, `Algebra.TensorProduct.isField_of_isAlgebraic`, `TensorProduct.toLinearEquiv_congrIsometry`, `PolynomialLaw.zero_def`, `TensorProduct.lid_tmul`, `Algebra.FormallySmooth.instTensorProduct`, `SemimoduleCat.hom_inv_leftUnitor`, `FGModuleCat.FGModuleCatCoevaluation_apply_one`, `LinearMap.BilinMap.baseChange_tmul`, `Module.Flat.eqLocus_lTensor_eq`, `QuadraticForm.tmul_tensorAssoc_apply`, `TensorProduct.exists_finite_submodule_left_of_finite`, `LinearMap.intrinsicStar_rTensor`, `Algebra.FormallyEtale.instTensorProduct`, `TensorProduct.piRight_symm_apply`, `Algebra.TensorProduct.congr_toLinearEquiv`, `AdicCompletion.ofTensorProductEquivOfFiniteNoetherian_symm_of`, `TensorProduct.gradedComm_one`, `TensorProduct.toLinearEquiv_commIsometry`, `TensorProduct.lift.tmul`, `finsuppTensorFinsupp'_symm_single_eq_single_one_tmul`, `TensorProduct.lTensorHomToHomLTensor_apply`, `Matrix.single_kroneckerTMul_single`, `BialgCat.tensorHom_def`, `Algebra.TensorProduct.tmul_mul_tmul`, `Coalgebra.sum_counit_tmul_map_eq`, `TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul`, `Module.Invertible.instTensorProduct_2`, `Submodule.baseChange_bot`, `Subalgebra.mulMap'_surjective`, `Submodule.comm_trans_rTensorOne`, `LinearMap.mulRight_tmul`, `LinearMap.smul_lTensor`, `TensorProduct.intrinsicStar_map`, `AdicCompletion.ofTensorProduct_bijective_of_finite_of_isNoetherian`, `Algebra.TensorProduct.instFree`, `TensorProduct.LieModule.map_tmul`, `Submodule.exists_fg_le_subset_range_rTensor_subtype`, `TensorProduct.rTensor_injective_of_forall_vanishesTrivially`, `ModuleCat.hom_hom_leftUnitor`, `LinearMap.map_comp_rTensor`, `LinearMap.IsSymm.tmul`, `TensorProduct.isPushout`, `DFinsupp.comul_comp_lapply`, `Module.rankAtStalk_eq_finrank_tensorProduct`, `TensorProduct.finsuppScalarRight_apply_tmul_apply`, `SemimoduleCat.MonoidalCategory.tensorμ_apply`, `Algebra.TensorProduct.leftComm_toLinearEquiv`, `LinearEquiv.baseChange_tmul`, `QuadraticForm.tmul_tensorComm_apply`, `Ideal.ResidueField.exists_smul_eq_tmul_one`, `kroneckerLinearEquiv_symm_kronecker`, `TensorProduct.finsuppLeft_apply`, `ModuleCat.hom_hom_rightUnitor`, `LinearMap.comm_comp_lTensor_comp_comm_eq`, `TensorProduct.mapBilinear_apply`, `finsuppTensorFinsuppRid_symm_single_smul`, `TensorProduct.prodRight_symm_tmul`, `TensorProduct.ext_iff_inner_right`, `TensorProduct.exists_finsupp_left`, `TensorProduct.gradedComm_symm`, `QuadraticForm.tensorLId_toLinearEquiv`, `Algebra.TensorProduct.congr_apply`, `TensorProduct.AlgebraTensorModule.dualDistrib_apply`, `Coalgebra.IsCocomm.comm_comp_comul`, `Algebra.TensorProduct.toLinearEquiv_tensorTensorTensorComm`, `Algebra.Generators.snd_comp_cotangentCompLocalizationAwayEquiv`, `Module.Flat.instTensorProduct`, `GradedTensorProduct.auxEquiv_mul`, `QuadraticForm.tmul_tensorRId_apply`, `TensorProduct.range_map_mono`, `TensorProduct.piRight_symm_single`, `Submodule.lTensorOne'_tmul`, `rank_tensorProduct`, `MvPolynomial.finite_universalFactorizationMap`, `MvPolynomial.rTensorAlgHom_toLinearMap`, `Submodule.rTensorOne'_tmul_one`, `coe_polyEquivTensor'_symm`, `baseChange_ext_iff`, `Subbimodule.coe_mk`, `Prod.comul_apply`, `Rep.finsuppTensorRight_hom_hom`, `QuotSMulTop.equivQuotTensor_naturality`, `Submodule.rTensorOne'_tmul`, `Matrix.conjTranspose_kroneckerTMul`, `MvPolynomial.universalFactorizationMapPresentation_map`, `Module.Invertible.rTensor_injective_iff`, `Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex`, `Algebra.TensorProduct.basisAux_tmul`, `TensorProduct.exists_finite_submodule_right_of_setFinite'`, `TensorProduct.AlgebraTensorModule.map_add_left`, `TensorProduct.AlgebraTensorModule.uncurry_apply`, `TensorProduct.map_comm`, `MvPolynomial.algebraTensorAlgEquiv_symm_X`, `LinearEquiv.congr_trans_rTensor`, `AlternatingMap.domCoprod'_apply`, `Submodule.LinearDisjoint.injective`, `Submodule.baseChange_eq_span`, `tensorKaehlerQuotKerSqEquiv_symm_tmul_D`, `Algebra.IsStandardSmooth.baseChange`, `Matrix.kroneckerTMulAlgEquiv_symm_apply`, `coe_polyEquivTensor'`, `Algebra.Unramified.baseChange`, `TensorProduct.AlgebraTensorModule.coe_lTensor`, `Coalgebra.rTensor_counit_comp_comul`, `Matrix.kroneckerTMulStarAlgEquiv_apply`, `Algebra.TensorProduct.includeRight_bijective`, `toMatrix_dualTensorHom`, `LinearIndependent.tmul_of_flat_left`, `Algebra.Generators.H1Cotangent.δAux_ofComp`, `Matrix.diagonal_kroneckerTMul_diagonal`, `TensorProduct.AlgebraTensorModule.homTensorHomMap_apply`, `Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_isDomain`, `PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux`, `Submodule.injective_tensorToSpan`, `AlgebraicGeometry.pullbackSpecIso_inv_fst`, `AlgCat.hom_inv_leftUnitor`, `CoalgCat.MonoidalCategoryAux.leftUnitor_hom_toLinearMap`, `AdicCompletion.ofTensorProduct_bijective_of_pi_of_fintype`, `RCLike.inner_tmul_eq`, `LinearMap.map_comp_lTensor`, `LieModule.instIsNilpotentTensor`, `Coalgebra.TensorProduct.map_tmul`, `TensorProduct.LieModule.coe_liftLie_eq_lift_coe`, `Matrix.diagonal_kroneckerTMul`, `CoalgHomClass.map_comp_comul`, `SemimoduleCat.hom_inv_associator`, `Module.Relations.Solution.IsPresentation.tensor`, `Module.Basis.baseChange_end`, `TensorProduct.lid'_apply_tmul`, `Algebra.TensorProduct.liftEquiv_apply`, `LinearEquiv.rTensor_refl`, `KaehlerDifferential.instSMulCommClassTensorProduct_1`, `TensorProduct.map_smul_right`, `TensorProduct.enorm_tmul`, `Module.Basis.baseChange_apply`, `CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc`, `Algebra.TensorProduct.not_isField_of_transcendental`, `Module.rankAtStalk_tensorProduct`, `LinearMap.lTensor_mul`, `Algebra.TensorProduct.productMap_range`, `Submodule.mulRightMap_eq_mulMap_comp`, `Algebra.TensorProduct.basis_repr_symm_apply'`, `TensorProduct.inner_assoc_assoc`, `kroneckerTMulLinearEquiv_mul`, `groupHomology.H1AddEquivOfIsTrivial_single`, `LinearEquiv.baseChange_zpow`, `kroneckerTMulLinearEquiv_symm_kroneckerTMul`, `ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm`, `Module.rankAtStalk_tensorProduct_of_isScalarTower`, `Module.Free.tensor`, `Bialgebra.TensorProduct.rid_toAlgEquiv`, `TensorProduct.gradedMul_one`, `QuadraticForm.tensorComm_toLinearEquiv`, `Algebra.TensorProduct.productMap_eq_comp_map`, `PointedCone.tmul_subset_maxTensorProduct`, `CliffordAlgebra.ofBaseChange_tmul_ι`, `KaehlerDifferential.tensorKaehlerEquiv_left_inv`, `QuadraticModuleCat.toIsometry_hom_leftUnitor`, `Algebra.TensorProduct.rid_tmul`, `Submodule.rTensorOne_tmul`, `IsLocalizedModule.rTensor`, `Algebra.TensorProduct.lmul'_comp_includeRight`, `QuadraticModuleCat.toIsometry_hom_rightUnitor`, `rTensor.inverse_of_rightInverse_comp_rTensor`, `TensorProduct.zero_tmul`, `Module.Presentation.tensor_G`, `IsBaseChange.equiv_symm_apply`, `TensorProduct.congr_symm_tmul`, `Algebra.pushoutDesc_apply`, `CommRingCat.coproductCocone_pt`, `Algebra.TensorProduct.cancelBaseChange_tmul`, `Algebra.TensorProduct.map_comp_id`, `Submodule.coe_mulMap_comp_eq`, `TensorProduct.AlgebraTensorModule.curry_apply`, `QuadraticForm.tensorLId_symm_apply`, `starLinearEquiv_tensor`, `Algebra.TensorProduct.mul_one`, `TensorProduct.exists_finite_submodule_left_of_finite'`, `TensorProduct.sum_tmul`, `TensorProduct.finsuppScalarRight_symm_apply_single`, `LinearIsometryEquiv.toLinearEquiv_lTensor`, `AlgCat.hom_hom_leftUnitor`, `TensorProduct.tmul_sum`, `Algebra.TensorProduct.mk_one_injective_of_isScalarTower`, `Module.Flat.iff_lTensor_injective`, `CliffordAlgebra.ofBaseChangeAux_ι`, `Ideal.ker_tensorProductMk_quotient`, `LinearEquiv.rTensor_symm_tmul`, `Bialgebra.comul_mul`, `CommAlgCat.coe_tensorObj`, `TensorProduct.AlgebraTensorModule.mapBilinear_apply`, `TensorProduct.piRightHom_tmul`, `LinearMap.lTensor_comm`, `TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk`, `tensorKaehlerQuotKerSqEquiv_tmul_D`, `HopfAlgebra.mul_antipode_rTensor_comul`, `LieSubmodule.lie_baseChange`, `TensorProduct.tensorQuotientEquiv_apply_mk_tmul`, `LinearMap.lTensor_id`, `TensorProduct.exists_finite_submodule_of_finite`, `Algebra.FormallyUnramified.one_tmul_sub_tmul_one_mul_elem`, `QuadraticForm.tensorDistrib_tmul`, `Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_left`, `LieModule.toModuleHom_apply`, `TensorProduct.map_one`, `GradedTensorProduct.mulHom_apply`, `rTensor.inverse_comp_rTensor`, `PointedCone.minTensorProduct_le_maxTensorProduct`, `PolyEquivTensor.invFun_add`, `TensorProduct.directSumRight_tmul_lof`, `OrthonormalBasis.tensorProduct_apply'`, `Module.Invertible.rTensor_bijective_iff`, `MultilinearMap.domCoprod'_apply`, `ModuleCat.hom_inv_rightUnitor`, `MvPolynomial.universalFactorizationMapPresentation_relation`, `Equiv.tensorProductAssoc_def`, `Algebra.TensorProduct.congr_refl`, `LinearMap.map_rTensor`, `ModuleCat.ExtendScalars.smul_tmul`, `QuadraticForm.tensorComm_apply`, `Subbimodule.coe_toSubbimoduleInt`, `Module.Flat.linearIndependent_one_tmul`, `TensorProduct.exists_multiset`, `Module.Flat.iff_rTensor_exact'`, `LieAlgebra.derivedSeries_baseChange`, `Algebra.Generators.Cotangent.exact`, `kroneckerTMulLinearEquiv_tmul`, `LinearMap.rTensor_comp_comm`, `Subalgebra.rTensorBot_tmul_one`, `TensorProduct.AlgebraTensorModule.restrictScalars_rTensor`, `QuadraticForm.tmul_comp_tensorMap`, `Module.Dual.baseChange_apply_tmul`, `LinearMap.rTensor_baseChange`, `Algebra.IsPushout.cancelBaseChangeAux_symm_tmul`, `Commute.tmul`, `Algebra.TensorProduct.map_surjective`, `TensorProduct.directSumLeft_symm_lof_tmul`, `BialgCat.whiskerRight_def`, `IsAzumaya.coe_tensorEquivEnd`, `AlgHom.tensorEqualizerEquiv_apply`, `Matrix.kroneckerTMul_add`, `PointedCone.tmul_subset_minTensorProduct`, `rTensor_mkQ`, `TensorProduct.lift_comp_map`, `TensorProduct.sum_tmul_eq_zero_of_vanishesTrivially`, `TensorProduct.tensorQuotEquivQuotSMul_symm_mk`, `Module.Relations.Solution.tensor_var`, `CommAlgCat.binaryCofan_inl`, `Module.Flat.tensorProduct_mapIncl_injective_of_left`, `TensorProduct.comm_trans_comm`, `PolynomialLaw.add_def_apply`, `QuadraticForm.tensorAssoc_symm_apply`, `Coalgebra.coassoc`, `MonoidAlgebra.tensorEquiv_tmul`, `Module.mem_freeLocus_iff_tensor`, `TensorProduct.AlgebraTensorModule.map_add_right`, `TensorProduct.ite_tmul`, `Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul`, `TensorProduct.Algebra.linearMap_comp_mul'`, `TensorProduct.map_injective_of_flat_flat`, `Algebra.Smooth.baseChange`, `Module.Flat.iff_lTensor_injectiveₛ`, `LieAlgebra.ExtendScalars.bracket_tmul`, `Algebra.TensorProduct.comm_comp_includeRight`, `TensorProduct.toLinearMap_congr`, `CliffordAlgebra.toBaseChange_ofBaseChange`, `LinearMap.lTensor_comp_rTensor`, `TensorProduct.rid_tmul`, `LinearMap.lTensor_zero`, `Submodule.tmul_mem_baseChange_of_mem`, `matrixEquivTensor_apply_single`, `CharacterModule.homEquiv_symm_apply_apply_apply`, `QuadraticModuleCat.toIsometry_inv_rightUnitor`, `LinearMap.adjoint_lTensor`, `Algebra.TensorProduct.cancelBaseChange_symm_tmul`, `MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap`, `TensorProduct.AlgebraTensorModule.map_one`, `MvPolynomial.coeff_rTensorAlgHom_tmul`, `PiTensorProduct.tmulEquivDep_symm_apply`, `Submodule.rTensorOne_tmul_one`, `DFinsupp.comul_comp_lsingle`, `Algebra.TensorProduct.comm_comp_includeLeft`, `Subbimodule.coe_toSubbimoduleNat`, `LinearMap.lTensor_comp_mk`, `KaehlerDifferential.instSMulCommClassTensorProduct`, `CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right`, `Module.Flat.baseChange`, `Module.Invertible.rTensorInv_leftInverse`, `TensorProduct.forall_vanishesTrivially_iff_forall_rTensor_injective`, `MatrixEquivTensor.invFun_smul`, `TensorProduct.single_tmul`, `finsuppTensorFinsuppRid_single_tmul_single`, `IsLocalRing.split_injective_iff_lTensor_residueField_injective`, `Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul`, `PolynomialLaw.isCompat`, `Algebra.Extension.contangentEquiv_tmul`, `PolynomialLaw.add_def`, `RingTheory.Sequence.IsWeaklyRegular.isWeaklyRegular_rTensor`, `TensorProduct.finsuppScalarLeft_apply_tmul_apply`, `TensorProduct.inner_comm_comm`, `LinearMap.polyCharpolyAux_baseChange`, `ModuleCat.MonoidalCategory.tensorObj`, `LinearMap.coe_rTensorHom`, `Algebra.TensorProduct.assoc_toLinearEquiv`, `LinearMap.baseChange_sub`, `Coalgebra.lift_lsmul_comp_counit_comp_comul`, `Algebra.TensorProduct.assoc_symm_tmul`, `Algebra.TensorProduct.opAlgEquiv_symm_apply`, `Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq`, `matrixEquivTensor_apply_symm`, `TensorProduct.map_mul`, `LieSubmodule.tmul_mem_baseChange_of_mem`, `QuadraticForm.tensorRId_toLinearEquiv`, `Bialgebra.TensorProduct.map_tmul`, `PolynomialLaw.toFun_smul`, `Subalgebra.mulMap_bot_right_eq`, `groupHomology.H1AddEquivOfIsTrivial_symm_apply`, `PiTensorProduct.tmulEquivDep_apply`, `Algebra.TensorProduct.linearEquivIncludeRange_symm_tmul`, `Algebra.TensorProduct.algEquivIncludeRange_tmul`, `Algebra.Smooth.exists_subalgebra_finiteType`, `MatrixEquivTensor.left_inv`, `TensorProduct.LieModule.lift_apply`, `CoalgCat.MonoidalCategoryAux.counit_tensorObj`, `TensorProduct.isBaseChange`, `TensorProduct.LieModule.lie_tmul_right`, `LaurentPolynomial.comul_C`, `TensorProduct.assocIsometry_apply`, `CliffordAlgebra.toBaseChange_comp_reverseOp`, `Finsupp.comul_single`, `HopfAlgebra.mul_antipode_rTensor_comul_apply`, `PrimeSpectrum.isHomeomorph_comap_of_isPurelyInseparable`, `DirectedSystem.lTensor`, `GradedTensorProduct.auxEquiv_tmul`, `KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange`, `Subalgebra.lTensorBot_symm_apply`, `TensorProduct.add_smul`, `Algebra.Etale.exists_subalgebra_fg`, `TensorProduct.AlgebraTensorModule.lTensor_comp`, `LinearIsometryEquiv.rTensor_apply`, `groupHomology.H1ToTensorOfIsTrivial_H1π_single`, `homTensorHomEquiv_toLinearMap`, `TensorProduct.map_bijective`, `KaehlerDifferential.submodule_span_range_eq_ideal`, `LinearMap.baseChange_neg`, `AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc`, `TensorProduct.SMul.aux_of`, `Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply`, `Algebra.TensorProduct.map_range`, `Module.finrank_tensorProduct`, `TensorProduct.gradedComm_of_zero_tmul`, `Algebra.TensorProduct.tmul_pow`, `ModuleCat.MonoidalCategory.tensorμ_apply`, `TensorProduct.isScalarTower_left`, `IsBaseChange.endHom_apply`, `LinearMap.mul''_apply`, `Module.Invertible.rTensorInv_injective`, `TensorProduct.AlgebraTensorModule.lTensor_mul`, `Algebra.TensorProduct.map_comp_includeRight`, `TensorProduct.piScalarRight_symm_single`, `MvPolynomial.ker_eval₂Hom_universalFactorizationMap`, `PolyEquivTensor.toFunAlgHom_apply_tmul_eq_smul`, `TensorProduct.sub_tmul`, `Algebra.TensorProduct.one_mul`, `TensorProduct.map₂_mk_top_top_eq_top`, `TensorPower.gMul_def`, `Module.Flat.iff_rTensor_exact`, `Subalgebra.tmul_mem_baseChange`, `LinearMap.baseChange_zero`, `SemimoduleCat.MonoidalCategory.associator_inv_apply`, `CommAlgCat.braiding_inv_hom`, `rTensor_exact`, `Algebra.Smooth.exists_finiteType`, `LinearMap.polyCharpolyAux_map_aeval`, `TensorProduct.directSumLeft_tmul`, `Algebra.TensorProduct.piRightHom_one`, `LinearMap.liftBaseChange_tmul`, `Submodule.mulMap_one_left_eq`, `TensorProduct.map_comp`, `TensorProduct.quotTensorEquivQuotSMul_symm_mk`, `Algebra.IsPushout.equiv_tmul`, `LinearMap.rTensor_surjective`, `AddMonoidAlgebra.tensorEquiv_tmul`, `BialgCat.tensorObj_def`, `ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal`, `CommAlgCat.associator_inv_hom`, `ModuleCat.ihom_coev_app`, `IsBaseChange.toDual_apply`, `TensorProduct.instIsCocomm`, `LinearIsometry.toLinearMap_rTensor`, `PolyEquivTensor.toFunLinear_tmul_apply`, `TensorProduct.smul_tmul'`, `TensorProduct.exists_finite_submodule_of_setFinite'`, `CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_left`, `Module.FaithfullyFlat.one_tmul_eq_zero_iff`, `DirectedSystem.rTensor`, `Algebra.TensorProduct.tensorTensorTensorComm_toLinearEquiv`, `Algebra.Generators.H1Cotangent.exact_map_δ'`, `AlgebraicGeometry.pullbackSpecIso_inv_fst_assoc`, `TensorProduct.eq_repr_basis_left`, `LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmul`, `Module.FaithfullyFlat.zero_iff_lTensor_zero`, `LinearMap.lTensor_bij_iff_rTensor_bij`, `Submodule.mulMap_comm_of_commute`, `Algebra.TensorProduct.ext_iff`, `TensorProduct.AlgebraTensorModule.map_mul`, `QuadraticForm.tmul_tensorLId_apply`, `MvPolynomial.rTensor_symm_apply_single`, `QuadraticForm.tensorLId_apply`, `ModuleCat.hom_hom_associator`, `IsLocalization.bijective_linearMap_mul'`, `LinearMap.lTensor_comp_apply`, `LinearIsometryEquiv.symm_rTensor`, `LinearMap.BilinForm.tensorDistribEquiv_tmul`, `LinearMap.trace_tensorProduct'`, `TensorProduct.commIsometry_symm`, `TensorProduct.leftComm_symm_tmul`, `KaehlerDifferential.D_tensorProductTo`, `LinearEquiv.lTensor_refl`, `Rep.finsuppTensorRight_inv_hom`, `QuotSMulTop.equivQuotTensor_naturality_mk`, `Submodule.mulMap_eq_mul'_comp_mapIncl`, `Module.Flat.iff_lTensor_preserves_injective_linearMapₛ`, `Algebra.TensorProduct.algEquivIncludeRange_toAlgHom`, `Module.Invertible.lTensor_injective_iff`, `AddMonoidAlgebra.tensorEquiv_symm_single`, `LieModule.toEnd_baseChange`, `LinearEquiv.baseChange_inv`, `Derivation.tensorProductTo_mul`, `TensorProduct.assoc_tensor''`, `contractLeft_apply`, `LinearMap.BilinMap.tensorDistrib_tmul`, `IsLocalization.Away.tensor`, `LineDeriv.tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp`, `QuadraticForm.comp_tensorRId_eq`, `HopfAlgCat.tensorHom_def`, `TensorProduct.LieModule.toLinearMap_map`, `AdicCompletion.tensor_map_id_left_eq_map`, `TensorProduct.range_map_eq_span_tmul`, `PolynomialLaw.toFun_add`, `Algebra.Generators.CotangentSpace.exact`, `Algebra.Generators.H1Cotangent.δAux_X`, `Algebra.TensorProduct.comm_symm_tmul`, `Coalgebra.sum_tmul_tmul_eq`, `CharacterModule.dual_rTensor_conj_homEquiv`, `TensorProduct.equivFinsuppOfBasisRight_apply`, `Submodule.mulLeftMap_eq_mulMap_comp`, `MonoidAlgebra.scalarTensorEquiv_symm_single`, `TensorProduct.counit_def`, `PointedCone.minTensorProduct_comm`, `LinearMap.mulLeft_tmul`, `Subbimodule.coe_toSubmodule`, `Matrix.add_kroneckerTMul`, `Algebra.TensorProduct.quotIdealMapEquivTensorQuot_symm_tmul`, `TensorProduct.directSum_symm_lof_tmul`, `TensorProduct.LinearIndepOn.tmul_of_flat_left`, `Module.FaithfullyFlat.rTensor_nontrivial`, `TensorProduct.tmul_single`, `CoalgCat.whiskerLeft_def`, `Module.FaithfullyFlat.tensorProduct_mk_injective`, `MultilinearMap.domCoprod_apply`, `MonoidAlgebra.comul_single`, `Algebra.FormallyUnramified.base_change`, `PolyEquivTensor.invFun_monomial`, `Subalgebra.linearDisjoint_iff_injective`, `Representation.smul_tprod_one_asModule`, `rTensorHomEquivHomRTensor_toLinearMap`, `LinearMap.lTensor_injective_of_exact_of_flat`, `AdicCompletion.ofTensorProduct_tmul`, `PolynomialLaw.neg_def`, `LinearMap.intrinsicStar_lTensor`, `MvPolynomial.rTensor_apply_monomial_tmul`, `LinearIndependent.tmul_of_isDomain`, `Subbimodule.coe_toSubmodule'`, `PiTensorProduct.tmulEquiv_apply`, `Module.Dual.baseChange_baseChange`, `TensorProduct.dualDistribInvOfBasis_apply`, `Pi.comul_coe_finsupp`, `isNilpotent_tensor_residueField_iff`, `BialgHomClass.map_comp_comulAlgHom`, `TensorProduct.lift_mk`, `dualTensorHom_prodMap_zero`, `PolyEquivTensor.toFunLinear_one_tmul_one`, `MultilinearMap.domCoprod_alternization`, `LinearMap.range_liftBaseChange`, `PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal`, `TensorProduct.enorm_assoc`, `NonUnitalAlgHom.comp_mul'`, `IsLocalization.tmul_mk'`, `TensorProduct.AlgebraTensorModule.rTensor_mul`, `TensorProduct.quotientTensorEquiv_apply_tmul_mk`, `LinearEquiv.coe_rTensor_symm`, `CommRingCat.coproductCoconeIsColimit_desc`, `Algebra.TensorProduct.piRight_tmul`, `AlgebraicGeometry.pullbackSpecIso_hom_fst`, `Algebra.TensorProduct.mul_assoc`, `SemimoduleCat.hom_hom_associator`, `TensorProduct.map_zero_left`, `TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse`, `PolyEquivTensor.left_inv`, `CliffordAlgebra.equivBaseChange_apply`, `Submodule.mulMap'_surjective`, `AlgCat.instMonoidalCategory.tensorObj_carrier`, `SemimoduleCat.MonoidalCategory.leftUnitor_naturality`, `TensorProduct.rightComm_tmul`, `TensorProduct.exists_finsupp_right`, `Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply`, `LinearMap.rTensor_map`, `dualTensorHomEquivOfBasis_toLinearMap`, `TensorProduct.finsuppScalarLeft_apply_tmul`, `TensorProduct.directSumRight_tmul`, `TensorProduct.gradedComm_tmul_algebraMap`, `Module.mem_support_iff_nontrivial_residueField_tensorProduct`, `TensorProduct.dist_tmul_le`, `Module.Invertible.rTensor_surjective_iff`, `Subalgebra.lTensorBot_tmul`, `MvPolynomial.tensorEquivSum_X_tmul_X`, `groupHomology.H1AddEquivOfIsTrivial_apply`, `TensorProduct.congr_mul`, `TensorProduct.norm_lid`, `SemimoduleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm`, `Rep.finsuppTensorLeft_inv_hom`, `TensorProduct.toLinearEquiv_assocIsometry`, `LinearMap.rTensor_comp`, `Module.Presentation.tensor_relation`, `LinearMap.rTensor_zero`, `LinearEquiv.rTensor_trans_apply`, `CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_right`, `MvPolynomial.coeff_rTensorAlgHom_monomial_tmul`, `TensorProduct.toIntegralClosure_injective_of_flat`, `TensorProduct.AlgebraTensorModule.map_smul_right`, `LinearEquiv.dilatransvection.baseChange`, `MvPolynomial.algebraTensorAlgEquiv_symm_map`, `TensorProduct.rid_symm_apply`, `Algebra.TensorProduct.productMap_right_apply`, `Bialgebra.TensorProduct.lid_toAlgEquiv`, `Module.End.baseChangeHom_apply_apply`, `Algebra.Generators.CotangentSpace.compEquiv_symm_inr`, `MvPolynomial.tensorEquivSum_C_tmul_one`, `TensorProduct.AlgebraTensorModule.map_comp`, `Subbimodule.coe_baseChange`, `Module.Basis.baseChange_repr_tmul`, `TensorProduct.nnnorm_assoc`, `Matrix.kroneckerAlgEquiv_symm_apply`, `Coalgebra.TensorProduct.assoc_tmul`, `TensorProduct.AlgebraTensorModule.lift_apply`, `Rep.leftRegularTensorTrivialIsoFree_inv_hom`, `TensorProduct.comul_tmul`, `Algebra.TensorProduct.basis_repr_symm_apply`, `Ideal.pi_mkQ_rTensor`, `finsuppTensorFinsuppLid_apply_apply`, `Prod.comul_comp_fst`, `polyEquivTensor_apply`, `TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm_tmul`, `Algebra.Presentation.algebraTensorAlgEquiv_symm_relation`, `TensorProduct.lcurry_apply`, `TensorProduct.curry_apply`, `Subalgebra.LinearDisjoint.val_mulMap_tmul`, `rTensor.inverse_apply`, `Submodule.mulMap_map_comp_eq`, `dualTensorHomEquivOfBasis_symm_cancel_left`, `TensorProduct.map_tmul`, `TensorProduct.mapIsometry_apply`, `Matrix.kroneckerTMul_smul`, `TensorProduct.smul_tmul_smul`, `Module.Invertible.rTensorEquiv_symm_apply_apply`, `Algebra.TensorProduct.right_isScalarTower`, `TensorProduct.comul_def`, `Algebra.TensorProduct.algebraMap_apply'`, `Module.Flat.iff_lift_lsmul_comp_subtype_injective`, `Algebra.TensorProduct.Algebra.TensorProduct.commRight_symm_tmul`, `Subalgebra.mulMap_range`, `TensorProduct.AlgebraTensorModule.congr_one`, `Coalgebra.TensorProduct.lid_toLinearEquiv`, `Algebra.instIsStandardOpenImmersionTensorProduct`, `TensorProduct.directSumRight'_restrict`, `Algebra.TensorProduct.lift_tmul`, `TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul`, `Submodule.FG.lTensor.directLimit_apply`, `RingHom.Finite.tensorProductMap`, `TensorProduct.lift.equiv_symm_apply`, `Subalgebra.centralizer_coe_range_includeLeft_eq_center_tensorProduct`, `TensorProduct.toLinearMap_mapIsometry`, `Algebra.Etale.baseChange`, `Subalgebra.rTensorBot_symm_apply`, `AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant`, `LinearMap.map_lTensor`, `TensorProduct.enorm_map`, `Prod.comul_comp_snd`, `Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop_tmul`, `TensorProduct.mapOfCompatibleSMul_tmul`, `Rep.linearization_δ_hom`, `Algebra.FormallySmooth.kerCotangentToTensor_injective_iff`, `KaehlerDifferential.derivationTensorProduct_algebraMap`, `Pi.comul_comp_proj`, `AdicCompletion.ofTensorProductEquivOfFiniteNoetherian_apply`, `Algebra.TensorProduct.lTensor_ker`, `TensorProduct.AlgebraTensorModule.rTensor_id`, `Matrix.kroneckerTMulBilinear_apply`, `TensorProduct.map_map_assoc`, `KaehlerDifferential.tensorProductTo_surjective`, `Algebra.TensorProduct.linearEquivIncludeRange_symm_toLinearMap`, `PointedCone.maxTensorProduct_comm`, `Coalgebra.rTensor_counit_comul`, `TensorProduct.commIsometry_apply`, `finsuppTensorFinsupp_symm_single`, `LinearMap.trace_tensorProduct`, `comp_dualTensorHom`, `Submodule.mulMap_comp_lTensor`, `TensorProduct.congrIsometry_symm`, `Coalgebra.TensorProduct.assoc_symm_tmul`, `MvPolynomial.pderiv_inr_universalFactorizationMap_X`, `Algebra.TensorProduct.natCast_def`, `Algebra.TensorProduct.tensorTensorTensorComm_tmul`, `TensorProduct.map_convMul_map`, `LinearMap.rTensor_exact_iff_lTensor_exact`, `TensorProduct.gradedMul_algebraMap`, `Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul`, `Matrix.trace_kroneckerTMul`, `IsIntegral.tmul`, `Derivation.tensorProductTo_tmul`, `Module.Flat.iff_rTensor_preserves_injective_linearMapₛ`, `IntermediateField.LinearDisjoint.isField_of_isAlgebraic'`, `TensorProduct.homTensorHomMap_apply`, `Submodule.lTensorOne_symm_apply`, `LinearMap.tensorEqLocus_tmul`, `TensorProduct.tmul_add`, `AddMonoidAlgebra.scalarTensorEquiv_symm_single`, `Submodule.tensorToSpan_apply_tmul`, `TensorProduct.gradedCommAux_comp_gradedCommAux`, `Algebra.baseChange_lmul`, `QuadraticForm.tensorAssoc_apply`, `TensorProduct.tensorTensorTensorComm_trans_tensorTensorTensorComm`, `finsuppTensorFinsuppRid_apply_apply`, `TensorProduct.toLinearMap_symm_lid`, `CoalgCat.MonoidalCategoryAux.comul_tensorObj`, `LinearMap.rTensor_comp_apply`, `Rep.finsuppTensorLeft_hom_hom`, `TensorProduct.tmul_of_gradedMul_of_tmul`, `Matrix.mul_kroneckerTMul_mul`, `LinearEquiv.coe_lTensor_symm`, `Submodule.lTensorOne'_one_tmul`, `Algebra.TensorProduct.lift_comp_includeRight'`, `map_dualTensorHom`, `PolynomialLaw.smul_def_apply`, `LieSubmodule.lieIdeal_oper_eq_tensor_map_range`, `TensorProduct.exists_finite_submodule_right_of_finite`, `Bialgebra.comul_pow`, `Algebra.TensorProduct.equivPiOfFiniteBasis_symm_apply`, `TensorProduct.AlgebraTensorModule.lTensor_one`, `TensorProduct.finsuppRight_symm_apply_single`, `TensorProduct.gradedComm_one_tmul`, `ModuleCat.MonoidalCategory.leftUnitor_def`, `LinearEquiv.comm_trans_rTensor_trans_comm_eq`, `TensorProduct.prodRight_tmul`, `KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap`, `Algebra.TensorProduct.quotIdealMapEquivTensorQuot_mk`, `Algebra.Generators.H1Cotangent.δ_eq_δAux`, `CliffordAlgebra.toBaseChange_involute`, `PolynomialLaw.toFun_neg`, `IsBaseChange.equiv_tmul`, `Bialgebra.comul_one`, `LinearMap.tensorProduct_apply`, `IsAddUnit.tmul_left`, `Rep.coinvariantsTensorMk_apply`, `Algebra.Generators.snd_cotangentCompLocalizationAwayEquiv`, `AlgebraicGeometry.pullbackSpecIso_hom_base_assoc`, `finsuppTensorFinsuppLid_single_tmul_single`, `Submodule.exists_fg_le_subset_range_rTensor_inclusion`, `Algebra.tensorH1CotangentOfIsLocalization_toLinearMap`, `Matrix.kroneckerTMulAlgEquiv_apply`, `Matrix.kroneckerTMul_diagonal`, `Rep.indMap_hom`, `MvPolynomial.algebraTensorAlgEquiv_tmul`, `Algebra.TensorProduct.comm_tmul`, `CharacterModule.uncurry_apply`, `Bialgebra.TensorProduct.assoc_toCoalgEquiv`, `Rep.homEquiv_symm_apply_hom`, `PrimeSpectrum.isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable`, `ModuleCat.extendScalarsComp_hom_app_one_tmul`, `Module.Invertible.lTensor_surjective_iff`, `IsLocalization.tensorRight`, `contractRight_apply`, `LinearMap.trace_eq_contract_of_basis`, `GradedTensorProduct.of_symm_of`, `KaehlerDifferential.span_range_eq_ideal`, `TensorProduct.liftAux.smul`, `Algebra.TensorProduct.lmul'_comp_includeLeft`, `Coalgebra.TensorProduct.rid_symm_apply`, `MatrixEquivTensor.right_inv`, `Algebra.TensorProduct.intCast_def`, `Algebra.Generators.CotangentSpace.map_toComp_injective`, `LinearMap.rTensor_range`, `TensorProduct.mk_surjective`, `Module.End.lTensorAlgHom_apply_apply`, `IsLocalization.tensor`, `Representation.ind_mk`, `TensorProduct.exists_finite_submodule_right_of_finite'`, `TensorProduct.add_tmul`, `ModuleCat.MonoidalCategory.tensorObj_def`, `TensorProduct.tensorTensorTensorAssoc_symm_tmul`, `TensorProduct.finsuppLeft_apply_tmul`, `PrimeSpectrum.continuous_tensorProductTo`, `Algebra.TensorProduct.opAlgEquiv_tmul`, `Module.Projective.tensorProduct`, `Algebra.TensorProduct.rid_toLinearEquiv`, `TensorProduct.AlgebraTensorModule.map_tmul`, `Bialgebra.TensorProduct.lid_toCoalgEquiv`, `PolynomialLaw.isCompat_apply'`, `Module.Invertible.bijective`, `TensorProduct.lidOfCompatibleSMul_tmul`, `Module.Invertible.lTensor_bijective_iff`, `LinearIsometryEquiv.toLinearIsometry_rTensor`, `LineDeriv.tensorLineDerivTwo_canonicalCovariantTensor_eq_sum`, `Pi.comul_single`, `Coalgebra.coassoc_apply`, `AlgebraicGeometry.pullbackSpecIso_hom_fst'_assoc`, `Coalgebra.TensorProduct.rid_toLinearEquiv`, `Module.Flat.iff_flat_tensorProduct`, `HopfAlgebra.mul_antipode_lTensor_comul_apply`, `CoalgCat.rightUnitor_def`, `Submodule.mulMap_comp_map_inclusion`, `TensorProduct.equivFinsuppOfBasisRight_symm`, `Bialgebra.TensorProduct.rid_symm_apply`, `LinearEquiv.lTensor_trans_apply`, `LinearMap.liftBaseChange_comp`, `MatrixEquivTensor.invFun_zero`, `Algebra.TensorProduct.algEquivIncludeRange_symm_toAlgHom`, `CoalgCat.tensorObj_carrier`, `Submodule.lTensorOne_tmul`, `HopfAlgCat.tensorObj_carrier`, `TensorProduct.norm_tmul`, `TensorProduct.directLimitLeft_tmul_of`, `MvPolynomial.aeval_one_tmul`, `MulOpposite.comul_def`, `Module.Flat.iff_rTensor_injectiveₛ`, `Subalgebra.comm_trans_lTensorBot`, `Submodule.LinearDisjoint.val_mulMap_tmul`, `Module.FaithfullyFlat.iff_flat_and_rTensor_faithful`, `Coalgebra.coassoc_symm`, `AlgebraicGeometry.pullbackSpecIso_inv_fst'`, `TensorProduct.lid'_symm_apply`, `Rep.coinvariantsTensorIndHom_mk_tmul_indVMk`, `IsAlgebraic.tmul`, `Rep.ihom_coev_app_hom`, `LaurentPolynomial.comul_C_mul_T`, `Prod.comul_comp_inl`, `HopfAlgCat.leftUnitor_def`, `Algebra.TensorProduct.comm_comp_map`, `TensorProduct.tmul_ite`, `MvPolynomial.universalFactorizationMapPresentation_algebra_smul`, `IsSMulRegular.rTensor`, `Matrix.toLinearEquiv_kroneckerAlgEquiv`, `PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal`, `TensorProduct.AlgebraTensorModule.curry_injective`, `LinearMap.lTensor_comp`, `PolynomialLaw.comp_toFun'`, `LinearMap.rid_comp_lTensor`, `TensorProduct.nnnorm_comm`, `Module.flat_iff`, `MvPolynomial.tensorEquivSum_one_tmul_X`, `FGModuleCat.FGModuleCatEvaluation_apply'`, `Matrix.det_kroneckerTMul`, `TensorProduct.map_ker`, `CommAlgCat.binaryCofan_inr`, `Submodule.exists_fg_le_eq_rTensor_subtype`, `TensorProduct.piScalarRight_apply`, `TensorProduct.exists_finset`, `Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux`, `LinearEquiv.lTensor_symm_tmul`, `Coalgebra.lTensor_counit_comp_comul`, `ModuleCat.hom_inv_leftUnitor`, `TensorProduct.exists_finite_submodule_of_setFinite`, `LinearEquiv.baseChange_pow`, `TensorProduct.exists_finite_submodule_left_of_setFinite'`, `Algebra.H1Cotangent.exact_map_δ`, `CliffordAlgebra.ofBaseChange_tmul_one`, `MvPolynomial.universalFactorizationMap_freeMonic`, `Coalgebra.TensorProduct.rid_tmul`, `Algebra.Generators.H1Cotangent.δ_comp_equiv`, `PolynomialLaw.id_apply'`, `MvPolynomial.universalFactorizationMapPresentation_val`, `TensorProduct.gradedCommAux_lof_tmul`, `Algebra.TensorProduct.prodRight_tmul`, `Algebra.TensorProduct.prodRight_tmul_snd`, `AlgebraicGeometry.diagonal_Spec_map`, `TensorProduct.directLimitLeft_symm_of_tmul`, `MvPolynomial.universalFactorizationMapPresentation_σ'`, `TensorProduct.norm_map`, `Algebra.TensorProduct.map_restrictScalars_comp_includeRight`, `LieAlgebra.derivedSeriesOfIdeal_baseChange`, `CommAlgCat.associator_hom_hom`, `Algebra.TensorProduct.liftEquiv_symm_apply_coe`, `Algebra.IsPushout.equiv_symm_algebraMap_right`, `Bialgebra.TensorProduct.rid_tmul`, `Submodule.map_range_rTensor_subtype_lid`, `QuadraticMap.Isometry.tmul_apply`, `LinearEquiv.baseChange_symm`, `LinearMap.mul'_tensor`, `CoalgCat.tensorObj_instCoalgebra`, `CliffordAlgebra.toBaseChange_ι`, `PointedCone.tmul_mem_minTensorProduct`, `Bialgebra.TensorProduct.lid_tmul`, `TensorProduct.comm_tmul`, `Subalgebra.centralizer_coe_image_includeLeft_eq_center_tensorProduct`, `TensorProduct.dualDistrib_apply`, `LinearMap.lTensor_pow`, `Module.Invertible.instTensorProduct`, `HopfAlgebra.mul_antipode_lTensor_comul`, `Module.Basis.tensorProduct_apply'`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe`, `LinearMap.rTensor_neg`, `Pi.comul_coe_dFinsupp`, `PolynomialLaw.isCompat_apply`, `TensorProduct.map_smul_left`, `Algebra.TensorProduct.includeRight_surjective`, `TensorProduct.congr_pow`, `IsLocalRing.subsingleton_tensorProduct`, `Algebra.TensorProduct.lmul'_toLinearMap`, `LinearMap.lTensor_map`, `TensorProduct.map_map_comp_assoc_symm_eq`, `TensorProduct.tensorQuotEquivQuotSMul_comp_mk`, `AdicCompletion.ofTensorProduct_naturality`, `MvPolynomial.scalarRTensor_symm_apply_single`, `Representation.smul_one_tprod_asModule`, `LinearIsometryEquiv.toLinearEquiv_rTensor`, `Subalgebra.val_mulMap'_tmul`, `TensorProduct.equivFinsuppOfBasisLeft_apply`, `Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_flat_right`, `QuadraticModuleCat.toIsometry_inv_leftUnitor`, `LinearIsometryEquiv.toLinearIsometry_lTensor`, `Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single`, `TensorProduct.comm_comp_comm_assoc`, `Ideal.comap_fiberIsoOfBijectiveResidueField_symm`, `Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_inl`, `Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_inr`, `Matrix.kroneckerTMul_apply`, `Coalgebra.TensorProduct.map_toLinearMap`, `TensorProduct.comm_comp_comm`, `Submodule.baseChange_top`, `LinearEquiv.rTensor_trans_lTensor`, `LieAlgebra.ExtendScalars.instLieModule`, `SemimoduleCat.hom_hom_leftUnitor`, `TensorProduct.AlgebraTensorModule.lift_tmul`, `RingHom.SurjectiveOnStalks.baseChange'`, `TensorProduct.antipode_def`, `Matrix.kroneckerTMul_assoc`, `Bialgebra.toLinearMap_comulAlgHom`, `LinearMap.convMul_apply`, `Algebra.injective_lift_lsmul`, `TensorProduct.lift_compr₂`, `KaehlerDifferential.range_kerCotangentToTensor`, `LinearMap.lid_comp_rTensor`, `Submodule.mulMap_op`, `IsTensorProduct.equiv_toLinearMap`, `LinearIndependent.tmul_of_flat_right`, `Prod.comul_comp_inr`, `Module.Flat.tensorProduct_mapIncl_injective_of_right`, `TensorProduct.lift_mk_compr₂ₛₗ`, `Derivation.liftKaehlerDifferential_apply`, `LieAlgebra.isSolvable_tensorProduct_iff`, `KaehlerDifferential.instIsScalarTowerTensorProduct_1`, `Finsupp.comul_comp_lsingle`, `Algebra.Presentation.baseChange_relation`, `KaehlerDifferential.DLinearMap_apply`, `Algebra.FinitePresentation.baseChange`, `Algebra.TensorProduct.lmul''_eq_lid_comp_mapOfCompatibleSMul`, `MvPolynomial.rTensor_apply`, `Algebra.TensorProduct.productMap_right`, `TensorProduct.ext_iff`, `TensorProduct.lift_comp_comm_eq`, `Rep.MonoidalClosed.linearHomEquivComm_symm_hom`, `TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero`, `TensorProduct.Algebra.moduleAux_apply`, `TensorProduct.map_range_eq_span_tmul`, `Subalgebra.LinearDisjoint.isDomain`, `IsBaseChange.linearMapLeftRightHom_apply`, `LinearIsometry.rTensor_apply`, `Module.Finite.base_change`, `TensorProduct.AlgebraTensorModule.congr_trans`, `LinearMap.mul'_comm`, `CoalgHomClass.map_comp_comul_apply`, `LinearIsometry.toLinearMap_lTensor`, `Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange`, `Coalgebra.Repr.eq`, `Algebra.Generators.CotangentSpace.fst_compEquiv_apply`, `LinearMap.lTensor_comp_map`, `TensorProduct.finsuppScalarLeft_apply`, `TensorProduct.LieModule.lieModule`, `TensorProduct.nndist_tmul_le`, `Submodule.lTensorOne_one_tmul`, `Algebra.FormallyUnramified.comp_sec`, `TensorProduct.assoc_tensor`, `AlgebraicGeometry.pullbackSpecIso_hom_fst'`, `PrimeSpectrum.mem_image_comap_zeroLocus_sdiff`, `Matrix.one_kroneckerTMul_one`, `Submodule.baseChange_span`, `KaehlerDifferential.tensorKaehlerEquiv_tmul_D`, `BialgCat.leftUnitor_def`, `MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix`, `TensorProduct.quotTensorEquivQuotSMul_comp_mk`, `Bialgebra.TensorProduct.lid_symm_apply`, `Bialgebra.TensorProduct.rid_toCoalgEquiv`, `AddMonoidAlgebra.scalarTensorEquiv_tmul`, `IntermediateField.LinearDisjoint.isField_of_forall`, `PointedCone.mem_maxTensorProduct`, `Coalgebra.TensorProduct.assoc_toLinearEquiv`, `SemimoduleCat.MonoidalCategory.rightUnitor_naturality`, `QuadraticForm.tmul_comp_tensorAssoc`, `TensorProduct.rTensorHomToHomRTensor_apply`, `IntermediateField.LinearDisjoint.isDomain'`, `TensorProduct.fromDirectLimit_of_tmul`, `LinearMap.tensorKerEquiv_apply`, `Representation.dualTensorHom_comm`, `LinearMap.baseChange_tmul`, `LinearMap.transvection.baseChange`, `Module.Basis.tensorProduct_repr_tmul_apply`, `MvPolynomial.algebraTensorAlgEquiv_symm_monomial`, `PolynomialLaw.ground_apply`, `QuadraticForm.associated_tmul`, `OrthonormalBasis.tensorProduct_apply`, `TensorProduct.neg_add_cancel`, `LinearMap.rTensor_add`, `Algebra.TensorProduct.ringHom_ext_iff`, `LinearEquiv.lTensor_refl_apply`, `TensorProduct.star_map_apply_eq_map_intrinsicStar`, `Module.Invertible.rightCancelEquiv_comp_rTensor_comp_symm`, `instNontrivialTensorProduct`, `TensorProduct.one_gradedMul`, `TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor`, `LinearEquiv.rTensor_trans`, `TensorProduct.finsuppScalarLeft_symm_apply_single`, `TensorProduct.piScalarRightHom_tmul`, `Algebra.TensorProduct.toLinearMap_map`, `QuadraticForm.tensorComm_symm`, `Algebra.TensorProduct.adjoin_tmul_eq_top`, `Bialgebra.mul_compr₂_comul`, `Algebra.TensorProduct.equivPiOfFiniteBasis_apply`, `Subalgebra.mulMap_tmul`, `LinearMap.rTensor_pow`, `Algebra.instIsStandardEtaleTensorProduct`, `TensorProduct.piRight_apply`, `Representation.ind_apply`, `TensorProduct.congrIsometry_apply`, `Algebra.TensorProduct.map_id_comp`, `LinearEquiv.baseChange_one`, `Algebra.TensorProduct.piScalarRight_tmul_apply`, `Equiv.tensorProductComm_def`, `Algebra.TensorProduct.lidOfCompatibleSMul_tmul`, `TensorProduct.map_pow`, `KaehlerDifferential.mulActionBaseChange_smul_zero`, `Module.FaithfullyFlat.nontrivial_tensorProduct_iff_left`, `Module.Flat.iff_rTensor_preserves_injective_linearMap'`, `LinearMap.rTensor_smul`, `TensorProduct.isPushout'`, `Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply`, `TensorProduct.toLinearMap_symm_rid`, `TensorProduct.assoc_tensor'`, `CoalgCat.MonoidalCategoryAux.rightUnitor_hom_toLinearMap`, `TensorProduct.nontrivial_of_linearMap_injective_of_flat_left`, `Module.Finite.tensorProduct`, `GradedTensorProduct.of_one`, `MvPolynomial.tensorEquivSum_X_tmul_one`, `LinearEquiv.lTensor_trans_rTensor`, `TensorProduct.AlgebraTensorModule.coe_rTensor`, `LieSubmodule.coe_baseChange`, `SpecialLinearGroup.baseChange_apply_coe`, `CoalgCat.leftUnitor_def`, `QuadraticMap.tensorDistrib_tmul`, `AlternatingMap.domCoprod_apply`, `CharacterModule.homEquiv_apply_apply`, `AlgebraicGeometry.pullbackSpecIso_hom_snd`, `AdicCompletion.tensor_map_id_left_injective_of_injective`, `Submodule.mulMap_range`, `TensorProduct.nnnorm_lid`, `Algebra.TensorProduct.map_bijective`, `TensorProduct.tensorQuotientEquiv_symm_apply_tmul_mk`, `Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply`, `Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_flat_left`, `GradedTensorProduct.symm_of_of`, `ModuleCat.MonoidalCategory.whiskerRight_def`, `matrixEquivTensor_apply`, `TensorProduct.lift_mk_compr₂`, `Module.FaithfullyFlat.iff_flat_and_lTensor_faithful`, `MatrixEquivTensor.toFunAlgHom_apply`, `LinearMap.BilinForm.baseChange_tmul`, `TensorProduct.gradedComm_of_tmul_of`, `TensorProduct.isTensorProduct`, `Algebra.TensorProduct.opAlgEquiv_symm_tmul`, `LinearMap.baseChange_mul`, `Rep.coinvariantsTensorIndInv_mk_tmul_indMk`, `IntermediateField.LinearDisjoint.isDomain`, `TensorProduct.map_surjective`, `Algebra.TensorProduct.lid_toLinearEquiv`, `rank_tensorProduct'`, `Module.Flat.iff_rTensor_injective'`, `LinearMap.baseChange_id`, `MvPolynomial.scalarRTensor_apply_tmul_apply`, `Algebra.FiniteType.baseChange`, `TensorProduct.directLimitRight_symm_of_tmul`, `Module.finrank_baseChange`, `PolynomialLaw.toFun_comp`, `IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expChar`, `TensorProduct.toMatrix_comm`, `LinearMap.lTensor_add`, `Algebra.TensorProduct.lid_symm_apply`, `dualTensorHomEquivOfBasis_apply`, `Submodule.FG.rTensor.directLimit_apply'`, `Orthonormal.tmul`, `groupHomology.H1AddEquivOfIsTrivial_symm_tmul`, `Module.Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap`, `TensorProduct.assoc_symm_tmul`, `LinearMap.ker_tensorProductMk`, `LieSubmodule.baseChange_top`, `TensorProduct.tmul_neg`, `Matrix.kroneckerStarAlgEquiv_apply`, `lTensor_mkQ`, `LinearMap.lTensor_inj_iff_rTensor_inj`, `Algebra.TensorProduct.leftComm_symm_tmul`, `TensorProduct.comm_symm_tmul`, `MvPolynomial.tensorEquivSum_C_tmul_C`, `TensorProduct.sum_tmul_basis_left_injective`, `Subalgebra.rTensorBot_tmul`, `LinearIsometryEquiv.symm_lTensor`, `LinearMap.comm_comp_rTensor_comp_comm_eq`, `TensorProduct.equivFinsuppOfBasisRight_symm_apply`, `QuadraticForm.associated_baseChange`, `ModuleCat.MonoidalCategory.tensorObj_carrier`, `KaehlerDifferential.map_liftBaseChange_smul`, `Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange`, `LinearMap.trace_baseChange`, `TensorProduct.exists_sum_tmul_eq`, `LinearMap.lTensor_tensor`, `LaurentPolynomial.comul_C_mul_T_self`, `CliffordAlgebra.ofBaseChange_comp_toBaseChange`, `le_comap_range_rTensor`, `MultilinearMap.domCoprodDep'_apply`, `TensorProduct.map_id`, `Algebra.TensorProduct.congr_symm`, `TensorProduct.AlgebraTensorModule.rightComm_symm`, `Algebra.FormallyUnramified.iff_exists_tensorProduct`, `IsBaseChange.toDualBaseChange_tmul`, `Coalgebra.comm_comp_comul`, `Algebra.TensorProduct.comm_toLinearEquiv`, `TensorProduct.instDirectedSystemCoeLinearMapIdLTensor`, `Rep.leftRegularTensorTrivialIsoFree_hom_hom`, `Bialgebra.TensorProduct.assoc_symm_tmul`, `TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ`, `TensorProduct.isScalarTower`, `Algebra.Generators.CotangentSpace.fst_compEquiv`, `Ideal.map_includeLeft_eq`, `TensorProduct.gradedComm_gradedMul`, `Bialgebra.TensorProduct.assoc_toAlgEquiv`, `Algebra.TensorProduct.rid_symm_apply`, `Algebra.TensorProduct.rTensor_ker`, `LinearEquiv.rTensor_tmul`, `Coalgebra.TensorProduct.lid_symm_apply`, `TensorProduct.rightComm_def`, `Algebra.TensorProduct.map_comp_includeLeft`, `Subalgebra.LinearDisjoint.isDomain_of_injective`, `TensorProduct.finsuppRight_apply_tmul_apply`, `TensorProduct.directSumRight_symm_lof_tmul`, `LinearEquiv.lTensor_trans`, `LieAlgebra.ExtendScalars.map_apply_tmul`, `Algebra.TensorProduct.mapOfCompatibleSMul_tmul`, `LieAlgebra.rootSpaceProduct_tmul`, `Module.Flat.iff_lTensor_injective'`, `LinearMap.charpoly_baseChange`, `TensorProduct.finsuppRight_apply_tmul`, `Algebra.EssFiniteType.baseChange`, `Submodule.mulMap_comp_rTensor`, `TensorProduct.map_zero_right`, `LinearIndepOn.tmul_of_isDomain`, `CommRingCat.coproductCocone_ι`, `polyEquivTensor_symm_apply_tmul_eq_smul`, `TensorProduct.AlgebraTensorModule.lcurry_apply`, `TensorProduct.comm_trans_rid`, `AlgebraicGeometry.pullbackSpecIso_hom_fst_assoc`, `AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective`, `LinearMap.baseChange_add`, `PrimeSpectrum.nontrivial_iff_mem_rangeComap`, `TensorProduct.toMatrix_map`, `Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single`, `TensorProduct.ext_iff_inner_right_threefold`, `LinearEquiv.lTensor_mul`, `IntermediateField.LinearDisjoint.isField_of_isAlgebraic`, `TensorProduct.exists_of_fg`, `Algebra.TensorProduct.comm_symm`, `Algebra.H1Cotangent.exact_δ_mapBaseChange`, `LinearMap.rTensor_mul`, `KaehlerDifferential.instIsScalarTowerTensorProduct_2`, `contractLeft_assoc_coevaluation'`, `TensorProduct.dualDistribEquivOfBasis_apply_apply`, `LinearMap.baseChangeHom_apply`, `OrthonormalBasis.tensorProduct_repr_tmul_apply`, `Matrix.kroneckerStarAlgEquiv_symm_apply`, `CommSemiring.comul_apply`, `Algebra.Generators.H1Cotangent.δ_map`, `TensorProduct.assocIsometry_symm_apply`, `Algebra.PreSubmersivePresentation.baseChange_ring`, `TensorProduct.inner_map_map`, `Algebra.TensorProduct.lift_includeLeft_includeRight`, `LinearMap.lTensor_tmul`, `LinearMap.lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm`, `TensorProduct.toLinearMap_mapInclIsometry`, `TensorProduct.lid_tensor`, `TensorProduct.coe_finsuppScalarRight'`, `KaehlerDifferential.mulActionBaseChange_smul_tmul`, `Algebra.FormallySmooth.iff_split_injection`, `TensorProduct.instIsCentralScalar`, `Algebra.TensorProduct.mul_apply`, `TensorProduct.lidIsometry_symm_apply`, `Algebra.TensorProduct.linearEquivIncludeRange_tmul`, `TensorProduct.range_mapIncl_mono`, `Algebra.Smooth.exists_subalgebra_fg`, `TensorProduct.AlgebraTensorModule.congr_tmul`, `Module.FaithfullyFlat.subsingleton_tensorProduct_iff_left`, `LinearEquiv.coe_rTensor`, `Algebra.TensorProduct.includeLeft_surjective`, `ModuleCat.ihom_ev_app`, `Algebra.TensorProduct.adjoin_one_tmul_image_eq_top`, `Representation.IndV.hom_ext_iff`, `PolynomialLaw.isCompat'`, `TensorProduct.one_smul`, `Pi.comul_comp_finsuppLcoeFun`, `TensorProduct.finsuppLeft'_apply`, `GradedTensorProduct.of_symm_one`, `TensorProduct.lift.equiv_apply`, `TensorProduct.finsuppRight_tmul_single`, `Rep.indResHomEquiv_symm_apply_hom`, `Subalgebra.centralizer_range_includeRight_eq_center_tensorProduct`, `TensorProduct.Algebra.mul'_comp_tensorTensorTensorComm`, `AlgHom.mulLeftRightMatrix.comp_inv`, `retractionOfSectionOfKerSqZero_tmul_D`, `Algebra.TensorProduct.one_def`, `IsLocalizedModule.map_lTensor`, `Module.Flat.rTensor_preserves_injective_linearMap`, `Module.Basis.baseChange_linearMap`, `LinearEquiv.congr_trans_lTensor`, `LinearEquiv.baseChange_trans`, `Module.Invertible.leftCancelEquiv_comp_lTensor_comp_symm`, `TensorProduct.toDirectLimit_tmul_of`, `Algebra.TensorProduct.includeLeftRingHom_apply`, `TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_tmul`, `Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg`, `TensorProduct.smulCommClass_left`, `Algebra.Presentation.baseChange_toGenerators`, `TensorProduct.quotTensorEquivQuotSMul_mk_tmul`, `ModuleCat.MonoidalCategory.associator_inv_apply`, `derivationQuotKerSq_mk`, `TensorProduct.uncurry_apply`, `TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ`, `MvPolynomial.universalFactorizationMapPresentation_jacobian`, `LinearMap.rTensor_tensor`, `TensorProduct.edist_tmul_le`, `Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap`, `TensorProduct.AlgebraTensorModule.lTensor_tmul`, `QuadraticModuleCat.hom_hom_associator`, `IsAzumaya.AlgHom.mulLeftRight_bij`, `Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap'`, `Rep.linearization_μ_hom`, `TensorProduct.liftAux.smulₛₗ`, `Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply`, `IsAddUnit.tmul_right`, `TensorProduct.includeRight_lid`, `Matrix.zero_kroneckerTMul`, `TensorProduct.tensorTensorTensorAssoc_tmul`, `SemimoduleCat.MonoidalCategory.associator_hom_apply`, `TensorProduct.finsuppLeft_apply_tmul_apply`, `instFinitePresentationTensorProduct`, `Module.Presentation.tensor_var`, `MvPolynomial.pderiv_inl_universalFactorizationMap_X`, `QuadraticModuleCat.hom_inv_associator`, `LieSubmodule.baseChange_bot`, `AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero`, `TensorProduct.eq_repr_basis_right`, `Algebra.TensorProduct.closure_range_union_range_eq_top`, `CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right`, `Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val`, `kroneckerLinearEquiv_tmul`, `SemimoduleCat.MonoidalCategory.id_tensorHom_id`, `AlgebraicGeometry.pullbackSpecIso_hom_snd_assoc`, `MvPolynomial.rTensorAlgHom_apply_eq`

---

← Back to Index