PiTensorProduct

📁 Source: Mathlib/LinearAlgebra/PiTensorProduct.lean

Statistics

Metric	Count
Definitions Eqv, distribMulAction', hasSMul', instAddCommGroup, instAddCommMonoid, instInhabited, instModule, instSMul, isEmptyEquiv, liftAddHom, liftAux, lifts, map, mapIncl, mapMonoidHom, mapMultilinear, map₂, module', piTensorHomMap, piTensorHomMapFun₂, piTensorHomMap₂, reindex, subsingletonEquiv, tmulEquiv, tmulEquivDep, tprod, tprodCoeff, «term⨂ₜ[_]_,_», «term⨂[_]_,_»	29
Theorems toPiTensorProduct, add_tprodCoeff, add_tprodCoeff', congr_symm_tprod, congr_tprod, ext, ext_iff, induction_on, induction_on', instIsScalarTower, instSMulCommClass, isEmptyEquiv_apply_tprod, isEmptyEquiv_symm_apply, isScalarTower', tprod, unique, unique', smul, liftAux_tprod, liftAux_tprodCoeff, lift_comp_map, lift_comp_reindex, lift_comp_reindex_symm, lift_reindex, lift_reindex_symm, lift_symm, lift_tprod, lifts_add, lifts_smul, lifts_zero, mapMonoidHom_apply, mapMultilinear_apply, map_comp, map_comp_reindex_eq, map_comp_reindex_symm, map_id, map_mul, map_one, map_pow, map_range_eq_span_tprod, map_reindex, map_reindex_symm, map_tprod, map_update_add, map_update_smul, map₂_tprod_tprod, mem_lifts_iff, nonempty_lifts, piTensorHomMapFun₂_add, piTensorHomMapFun₂_smul, piTensorHomMap_tprod_eq_map, piTensorHomMap_tprod_tprod, piTensorHomMap₂_tprod_tprod_tprod, reindex_comp_tprod, reindex_refl, reindex_reindex, reindex_symm, reindex_tprod, reindex_trans, smulCommClass', smul_add, smul_tprodCoeff, smul_tprodCoeff', smul_tprodCoeff_aux, span_tprod_eq_top, subsingletonEquiv_apply_tprod, subsingletonEquiv_symm_apply, subsingletonEquiv_symm_apply', tmulEquivDep_apply, tmulEquivDep_symm_apply, tmulEquiv_apply, tmulEquiv_symm_apply, tprodCoeff_eq_smul_tprod, tprod_eq_tprodCoeff_one, zero_tprodCoeff, zero_tprodCoeff'	76
Total	105

FreeAddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toPiTensorProduct 📖	mathematical	—	AddCon.toQuotient FreeAddMonoid AddSemigroup.toAdd AddMonoid.toAddSemigroup AddRightCancelMonoid.toAddMonoid AddCancelMonoid.toAddRightCancelMonoid instAddCancelMonoid addConGen PiTensorProduct.Eqv PiTensorProduct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup PiTensorProduct.instAddCommMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid PiTensorProduct.instSMul DFunLike.coe MultilinearMap CommSemiring.toSemiring PiTensorProduct.instModule MultilinearMap.instFunLikeForall PiTensorProduct.tprod Equiv EquivLike.toFunLike Equiv.instEquivLike toList	—	toList_nil toList_cons PiTensorProduct.tprodCoeff_eq_smul_tprod

PiTensorProduct

Definitions

Name	Category	Theorems
Eqv 📖	CompData	1 math math: FreeAddMonoid.toPiTensorProduct
distribMulAction' 📖	CompOp	3 math math: mapL_smul, piTensorHomMapFun₂_smul, map_update_smul
hasSMul' 📖	CompOp	4 math math: smulCommClass', smul_tprodCoeff', isScalarTower', smul_add
instAddCommGroup 📖	CompOp	15 math math: mapL_smul, projectiveSeminorm_apply, projectiveSeminorm_tprod_le, injectiveSeminorm_le_projectiveSeminorm, norm_eval_le_injectiveSeminorm, dualSeminorms_bounded, injectiveSeminorm_apply, mapLMultilinear_apply_apply, toDualContinuousMultilinearMap_le_projectiveSeminorm, norm_eval_le_projectiveSeminorm, injectiveSeminorm_tprod_le, exteriorPower.toTensorPower_apply_ιMulti, mapLMultilinear_opNorm, injectiveSeminorm_def, mapLMultilinear_toFun_apply
instAddCommMonoid 📖	CompOp	167 math math: mapL_id, TensorAlgebra.ofDirectSum_of_tprod, lift_reindex, lift.tprod, liftAlgHom_apply, tmulEquiv_symm_apply, mapLMonoidHom_apply, isEmptyEquiv_apply_tprod, dualDistribEquivOfBasis_symm_apply, FreeAddMonoid.toPiTensorProduct, TensorPower.cast_cast, ofDirectSumEquiv_tprod_lof, lift_reindex_symm, map_reindex_symm, reindex_reindex, subsingletonEquiv_symm_apply, TensorPower.cast_trans, TensorAlgebra.toDirectSum_tensorPower_tprod, TensorPower.gMul_eq_coe_linearMap, reindex_refl, SemiconjBy.tprod, toDualContinuousMultilinearMap_apply_apply, mul_assoc, map_comp, mapL_one, mapL_smul, TensorPower.algebraMap₀_mul, TensorAlgebra.toDirectSum_ofDirectSum, reindex_comp_tprod, lifts_add, tprod_prod, ofFinsuppEquiv'_tprod_single, TensorPower.cast_symm, subsingletonEquiv_apply_tprod, projectiveSeminorm_tprod_le, ofDirectSumEquiv_symm_lof_tprod, tprodL_toFun, ofFinsuppEquiv_tprod_single, TensorPower.mul_assoc, congr_symm_tprod, constantBaseRingEquiv_tprod, TensorPower.algebraMap₀_one, TensorAlgebra.equivDirectSum_apply, liftAux.smul, mapL_coe, ofFinsuppEquiv_symm_single_tprod, reindex_trans, liftIsometry_tprodL, one_def, reindex_tprod, tprodMonoidHom_apply, TensorPower.galgebra_toFun_def, piTensorHomMap_tprod_tprod, lifts_zero, norm_eval_le_injectiveSeminorm, tprodCoeff_eq_smul_tprod, TensorPower.tprod_mul_tprod, liftEquiv_symm_apply, reindex_symm, liftEquiv_apply, liftAux_tprodCoeff, TensorPower.algebraMap₀_eq_smul_one, ofDFinsuppEquiv_tprod_apply, dualDistribInvOfBasis_apply, mapL_mul, zero_tprodCoeff', mapL_comp, piTensorHomMap_tprod_eq_map, singleAlgHom_apply, lift_comp_reindex, dualDistribEquivOfBasis_apply_apply, TensorPower.multilinearMapToDual_apply_tprod, map₂_tprod_tprod, TensorAlgebra.ofDirectSum_toDirectSum, map_mul, TensorPower.mul_one, ofFinsuppEquiv_apply, map_one, mapMultilinear_apply, dualDistrib_apply, ext_iff, TensorPower.toTensorAlgebra_gMul, TensorPower.toTensorAlgebra_gOne, tprod_eq_tprodCoeff_one, isEmptyEquiv_symm_apply, subsingletonEquiv_symm_apply', SymmetricPower.range_mk, piTensorHomMapFun₂_smul, tmulEquivDep_symm_apply, liftAux_tprod, piTensorHomMap₂_tprod_tprod_tprod, tmulEquivDep_apply, mul_def, mem_lifts_iff, TensorAlgebra.toDirectSum_comp_ofDirectSum, ofDFinsuppEquiv_tprod_single, map_tprod, TensorPower.algebraMap₀_mul_algebraMap₀, mapLMultilinear_apply_apply, TensorPower.gMul_def, TensorPower.list_prod_gradedMonoid_mk_single, mapL_apply, liftIsometry_comp_mapL, one_mul, liftIsometry_symm_apply, tprod_noncommProd, TensorPower.cast_refl, piTensorHomMapFun₂_add, mul_one, tmulEquiv_apply, map_comp_reindex_symm, mapL_opNorm, toDualContinuousMultilinearMap_le_projectiveSeminorm, TensorPower.cast_tprod, dualDistrib_dualDistribInvOfBasis_right_inverse, mul_tprod_tprod, TensorPower.cast_eq_cast, tprodL_apply, lift_tprod, liftIsometry_apply_apply, TensorPower.gOne_def, TensorPower.one_mul, norm_eval_le_projectiveSeminorm, TensorAlgebra.equivDirectSum_symm_apply, lift_comp_map, add_tprodCoeff, TensorAlgebra.mk_reindex_fin_cast, Commute.tprod, ofFinsuppEquiv'_apply_apply, mapL_pow, map_reindex, TensorPower.mul_algebraMap₀, TensorAlgebra.mk_reindex_cast, mapMonoidHom_apply, lift_comp_reindex_symm, map_update_smul, ofDFinsuppEquiv_symm_single_tprod, span_tprod_eq_top, map_comp_reindex_eq, map_update_add, TensorPower.toTensorAlgebra_galgebra_toFun, TensorAlgebra.toDirectSum_ι, zero_tprodCoeff, ofDirectSumEquiv_tprod_apply, injectiveSeminorm_tprod_le, Basis.piTensorProduct_repr_tprod_apply, TensorAlgebra.ofDirectSum_comp_toDirectSum, mapL_add, mul_comm, exteriorPower.toTensorPower_apply_ιMulti, map_pow, tprod_mul_tprod, dualDistrib_dualDistribInvOfBasis_left_inverse, algebraMap_apply, smul_add, smul_tprod_mul_smul_tprod, mapLMultilinear_opNorm, TensorPower.toTensorAlgebra_tprod, Basis.piTensorProduct_apply, congr_tprod, map_range_eq_span_tprod, add_tprodCoeff', map_id, mapLMultilinear_toFun_apply, TensorPower.pairingDual_tprod_tprod, tprodL_coe, lift_symm
instInhabited 📖	CompOp	—
instModule 📖	CompOp	161 math math: mapL_id, TensorAlgebra.ofDirectSum_of_tprod, lift_reindex, lift.tprod, liftAlgHom_apply, tmulEquiv_symm_apply, mapLMonoidHom_apply, isEmptyEquiv_apply_tprod, dualDistribEquivOfBasis_symm_apply, FreeAddMonoid.toPiTensorProduct, TensorPower.cast_cast, ofDirectSumEquiv_tprod_lof, lift_reindex_symm, map_reindex_symm, reindex_reindex, subsingletonEquiv_symm_apply, TensorPower.cast_trans, TensorAlgebra.toDirectSum_tensorPower_tprod, TensorPower.gMul_eq_coe_linearMap, reindex_refl, SemiconjBy.tprod, toDualContinuousMultilinearMap_apply_apply, mul_assoc, map_comp, mapL_one, mapL_smul, TensorPower.algebraMap₀_mul, TensorAlgebra.toDirectSum_ofDirectSum, reindex_comp_tprod, tprod_prod, ofFinsuppEquiv'_tprod_single, TensorPower.cast_symm, subsingletonEquiv_apply_tprod, projectiveSeminorm_tprod_le, ofDirectSumEquiv_symm_lof_tprod, tprodL_toFun, ofFinsuppEquiv_tprod_single, TensorPower.mul_assoc, congr_symm_tprod, constantBaseRingEquiv_tprod, TensorPower.algebraMap₀_one, TensorAlgebra.equivDirectSum_apply, mapL_coe, ofFinsuppEquiv_symm_single_tprod, reindex_trans, liftIsometry_tprodL, one_def, reindex_tprod, tprodMonoidHom_apply, TensorPower.galgebra_toFun_def, piTensorHomMap_tprod_tprod, norm_eval_le_injectiveSeminorm, tprodCoeff_eq_smul_tprod, TensorPower.tprod_mul_tprod, liftEquiv_symm_apply, reindex_symm, liftEquiv_apply, TensorPower.algebraMap₀_eq_smul_one, ofDFinsuppEquiv_tprod_apply, dualDistribInvOfBasis_apply, mapL_mul, mapL_comp, piTensorHomMap_tprod_eq_map, singleAlgHom_apply, lift_comp_reindex, dualDistribEquivOfBasis_apply_apply, TensorPower.multilinearMapToDual_apply_tprod, map₂_tprod_tprod, TensorAlgebra.ofDirectSum_toDirectSum, dualSeminorms_bounded, map_mul, TensorPower.mul_one, ofFinsuppEquiv_apply, injectiveSeminorm_apply, map_one, mapMultilinear_apply, dualDistrib_apply, ext_iff, TensorPower.toTensorAlgebra_gMul, TensorPower.toTensorAlgebra_gOne, tprod_eq_tprodCoeff_one, isEmptyEquiv_symm_apply, subsingletonEquiv_symm_apply', SymmetricPower.range_mk, piTensorHomMapFun₂_smul, tmulEquivDep_symm_apply, liftAux_tprod, piTensorHomMap₂_tprod_tprod_tprod, tmulEquivDep_apply, mul_def, mem_lifts_iff, TensorAlgebra.toDirectSum_comp_ofDirectSum, ofDFinsuppEquiv_tprod_single, map_tprod, TensorPower.algebraMap₀_mul_algebraMap₀, mapLMultilinear_apply_apply, TensorPower.gMul_def, TensorPower.list_prod_gradedMonoid_mk_single, mapL_apply, liftIsometry_comp_mapL, one_mul, liftIsometry_symm_apply, tprod_noncommProd, TensorPower.cast_refl, piTensorHomMapFun₂_add, mul_one, tmulEquiv_apply, map_comp_reindex_symm, mapL_opNorm, toDualContinuousMultilinearMap_le_projectiveSeminorm, TensorPower.cast_tprod, dualDistrib_dualDistribInvOfBasis_right_inverse, mul_tprod_tprod, TensorPower.cast_eq_cast, tprodL_apply, lift_tprod, liftIsometry_apply_apply, TensorPower.gOne_def, TensorPower.one_mul, norm_eval_le_projectiveSeminorm, TensorAlgebra.equivDirectSum_symm_apply, lift_comp_map, TensorAlgebra.mk_reindex_fin_cast, Commute.tprod, ofFinsuppEquiv'_apply_apply, mapL_pow, map_reindex, TensorPower.mul_algebraMap₀, TensorAlgebra.mk_reindex_cast, mapMonoidHom_apply, lift_comp_reindex_symm, map_update_smul, ofDFinsuppEquiv_symm_single_tprod, span_tprod_eq_top, map_comp_reindex_eq, map_update_add, TensorPower.toTensorAlgebra_galgebra_toFun, TensorAlgebra.toDirectSum_ι, ofDirectSumEquiv_tprod_apply, injectiveSeminorm_tprod_le, Basis.piTensorProduct_repr_tprod_apply, TensorAlgebra.ofDirectSum_comp_toDirectSum, mapL_add, mul_comm, exteriorPower.toTensorPower_apply_ιMulti, map_pow, tprod_mul_tprod, dualDistrib_dualDistribInvOfBasis_left_inverse, algebraMap_apply, smul_tprod_mul_smul_tprod, mapLMultilinear_opNorm, TensorPower.toTensorAlgebra_tprod, Basis.piTensorProduct_apply, congr_tprod, map_range_eq_span_tprod, map_id, injectiveSeminorm_def, mapLMultilinear_toFun_apply, TensorPower.pairingDual_tprod_tprod, tprodL_coe, lift_symm
instSMul 📖	CompOp	24 math math: FreeAddMonoid.toPiTensorProduct, SymmetricPower.smul, lifts_smul, projectiveSeminorm_apply, TensorPower.algebraMap₀_mul, projectiveSeminorm_tprod_le, instSMulCommClass, liftAux.smul, injectiveSeminorm_le_projectiveSeminorm, norm_eval_le_injectiveSeminorm, tprodCoeff_eq_smul_tprod, TensorPower.algebraMap₀_eq_smul_one, dualDistribInvOfBasis_apply, injectiveSeminorm_apply, isEmptyEquiv_symm_apply, piTensorHomMapFun₂_smul, mem_lifts_iff, toDualContinuousMultilinearMap_le_projectiveSeminorm, norm_eval_le_projectiveSeminorm, TensorPower.mul_algebraMap₀, injectiveSeminorm_tprod_le, smul_tprod_mul_smul_tprod, instIsScalarTower, injectiveSeminorm_def
isEmptyEquiv 📖	CompOp	2 math math: isEmptyEquiv_apply_tprod, isEmptyEquiv_symm_apply
liftAddHom 📖	CompOp	—
liftAux 📖	CompOp	5 math math: liftAux.smul, liftAux_tprodCoeff, liftAux_tprod, mapLMultilinear_apply_apply, mapLMultilinear_toFun_apply
lifts 📖	CompOp	5 math math: projectiveSeminorm_apply, bddBelow_projectiveSemiNormAux, lifts_zero, mem_lifts_iff, nonempty_lifts
map 📖	CompOp	19 math math: map_reindex_symm, map_comp, mapL_coe, piTensorHomMap_tprod_eq_map, map_mul, map_one, mapMultilinear_apply, map_tprod, mapL_apply, map_comp_reindex_symm, lift_comp_map, map_reindex, mapMonoidHom_apply, map_update_smul, map_comp_reindex_eq, map_update_add, map_pow, map_range_eq_span_tprod, map_id
mapIncl 📖	CompOp	—
mapMonoidHom 📖	CompOp	1 math math: mapMonoidHom_apply
mapMultilinear 📖	CompOp	1 math math: mapMultilinear_apply
map₂ 📖	CompOp	1 math math: map₂_tprod_tprod
module' 📖	CompOp	—
piTensorHomMap 📖	CompOp	3 math math: piTensorHomMap_tprod_tprod, piTensorHomMap_tprod_eq_map, dualDistribEquivOfBasis_apply_apply
piTensorHomMapFun₂ 📖	CompOp	2 math math: piTensorHomMapFun₂_smul, piTensorHomMapFun₂_add
piTensorHomMap₂ 📖	CompOp	1 math math: piTensorHomMap₂_tprod_tprod_tprod
reindex 📖	CompOp	16 math math: lift_reindex, lift_reindex_symm, map_reindex_symm, reindex_reindex, reindex_refl, reindex_comp_tprod, reindex_trans, reindex_tprod, reindex_symm, lift_comp_reindex, map_comp_reindex_symm, TensorAlgebra.mk_reindex_fin_cast, map_reindex, TensorAlgebra.mk_reindex_cast, lift_comp_reindex_symm, map_comp_reindex_eq
subsingletonEquiv 📖	CompOp	3 math math: subsingletonEquiv_symm_apply, subsingletonEquiv_apply_tprod, subsingletonEquiv_symm_apply'
tmulEquiv 📖	CompOp	2 math math: tmulEquiv_symm_apply, tmulEquiv_apply
tmulEquivDep 📖	CompOp	2 math math: tmulEquivDep_symm_apply, tmulEquivDep_apply
tprod 📖	CompOp	74 math math: TensorAlgebra.ofDirectSum_of_tprod, lift.tprod, tmulEquiv_symm_apply, isEmptyEquiv_apply_tprod, FreeAddMonoid.toPiTensorProduct, ofDirectSumEquiv_tprod_lof, subsingletonEquiv_symm_apply, TensorAlgebra.toDirectSum_tensorPower_tprod, SemiconjBy.tprod, reindex_comp_tprod, tprod_prod, ofFinsuppEquiv'_tprod_single, subsingletonEquiv_apply_tprod, projectiveSeminorm_tprod_le, ofDirectSumEquiv_symm_lof_tprod, tprodL_toFun, ofFinsuppEquiv_tprod_single, congr_symm_tprod, constantBaseRingEquiv_tprod, ofFinsuppEquiv_symm_single_tprod, one_def, reindex_tprod, tprodMonoidHom_apply, piTensorHomMap_tprod_tprod, tprodCoeff_eq_smul_tprod, TensorPower.tprod_mul_tprod, ofDFinsuppEquiv_tprod_apply, dualDistribInvOfBasis_apply, piTensorHomMap_tprod_eq_map, singleAlgHom_apply, TensorPower.multilinearMapToDual_apply_tprod, map₂_tprod_tprod, ofFinsuppEquiv_apply, dualDistrib_apply, ext_iff, tprod_eq_tprodCoeff_one, isEmptyEquiv_symm_apply, subsingletonEquiv_symm_apply', tmulEquivDep_symm_apply, liftAux_tprod, piTensorHomMap₂_tprod_tprod_tprod, tmulEquivDep_apply, mem_lifts_iff, ofDFinsuppEquiv_tprod_single, map_tprod, TensorPower.list_prod_gradedMonoid_mk_single, one_mul, tprod_noncommProd, mul_one, tmulEquiv_apply, TensorPower.cast_tprod, mul_tprod_tprod, tprodL_apply, lift_tprod, TensorPower.gOne_def, Commute.tprod, ofFinsuppEquiv'_apply_apply, ofDFinsuppEquiv_symm_single_tprod, span_tprod_eq_top, TensorAlgebra.toDirectSum_ι, ofDirectSumEquiv_tprod_apply, injectiveSeminorm_tprod_le, Basis.piTensorProduct_repr_tprod_apply, exteriorPower.toTensorPower_apply_ιMulti, tprod_mul_tprod, algebraMap_apply, smul_tprod_mul_smul_tprod, TensorPower.toTensorAlgebra_tprod, Basis.piTensorProduct_apply, congr_tprod, map_range_eq_span_tprod, TensorPower.pairingDual_tprod_tprod, tprodL_coe, lift_symm
tprodCoeff 📖	CompOp	10 math math: tprodCoeff_eq_smul_tprod, liftAux_tprodCoeff, zero_tprodCoeff', tprod_eq_tprodCoeff_one, smul_tprodCoeff_aux, smul_tprodCoeff', smul_tprodCoeff, add_tprodCoeff, zero_tprodCoeff, add_tprodCoeff'
«term⨂ₜ[_]_,_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_tprodCoeff 📖	mathematical	—	PiTensorProduct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoid tprodCoeff Function.update	—	Quotient.sound'
add_tprodCoeff' 📖	mathematical	—	PiTensorProduct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoid tprodCoeff Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Quotient.sound'
congr_symm_tprod 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiTensorProduct instAddCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm congr MultilinearMap MultilinearMap.instFunLikeForall tprod	—	RingHomInvPair.ids map_tprod
congr_tprod 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiTensorProduct instAddCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike congr MultilinearMap MultilinearMap.instFunLikeForall tprod	—	RingHomInvPair.ids map_tprod
ext 📖	—	LinearMap.compMultilinearMap PiTensorProduct CommSemiring.toSemiring instAddCommMonoid instModule tprod	—	—	LinearMap.ext induction_on' tprodCoeff_eq_smul_tprod LinearMap.map_smul MultilinearMap.congr_fun LinearMap.map_add
ext_iff 📖	mathematical	—	LinearMap.compMultilinearMap PiTensorProduct CommSemiring.toSemiring instAddCommMonoid instModule tprod	—	ext
induction_on 📖	—	PiTensorProduct instSMul DFunLike.coe MultilinearMap CommSemiring.toSemiring instAddCommMonoid instModule MultilinearMap.instFunLikeForall tprod AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—	induction_on'
induction_on' 📖	—	tprodCoeff PiTensorProduct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoid	—	—	zero_tprodCoeff AddCon.induction_on
instIsScalarTower 📖	mathematical	—	IsScalarTower PiTensorProduct Algebra.toSMul CommSemiring.toSemiring Algebra.id instSMul	—	isScalarTower' IsScalarTower.right
instSMulCommClass 📖	mathematical	—	SMulCommClass PiTensorProduct instSMul	—	smulCommClass' Algebra.to_smulCommClass
isEmptyEquiv_apply_tprod 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiTensorProduct instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike isEmptyEquiv MultilinearMap MultilinearMap.instFunLikeForall tprod AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	lift.tprod
isEmptyEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiTensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid Semiring.toModule instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm isEmptyEquiv instSMul MultilinearMap MultilinearMap.instFunLikeForall tprod isEmptyElim	—	RingHomInvPair.ids
isScalarTower' 📖	mathematical	—	IsScalarTower PiTensorProduct hasSMul'	—	induction_on' smul_assoc smul_add
liftAux_tprod 📖	mathematical	—	DFunLike.coe AddMonoidHom PiTensorProduct AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid AddMonoidHom.instFunLike liftAux MultilinearMap CommSemiring.toSemiring instModule MultilinearMap.instFunLikeForall tprod	—	AddCon.lift_coe one_smul
liftAux_tprodCoeff 📖	mathematical	—	DFunLike.coe AddMonoidHom PiTensorProduct AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid AddMonoidHom.instFunLike liftAux tprodCoeff SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction MultilinearMap MultilinearMap.instFunLikeForall	—	—
lift_comp_map 📖	mathematical	—	LinearMap.comp PiTensorProduct CommSemiring.toSemiring instAddCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe LinearEquiv RingHomInvPair.ids MultilinearMap LinearMap MultilinearMap.addCommMonoid LinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike lift map MultilinearMap.compLinearMap	—	ext RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_self MultilinearMap.ext map_tprod lift.tprod
lift_comp_reindex 📖	mathematical	—	LinearMap.comp PiTensorProduct DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CommSemiring.toSemiring instAddCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv RingHomInvPair.ids MultilinearMap LinearMap MultilinearMap.addCommMonoid LinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.module LinearEquiv.instEquivLike lift LinearEquiv.toLinearMap reindex LinearEquiv.symm MultilinearMap.domDomCongrLinearEquiv'	—	ext RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_self MultilinearMap.ext lift.tprod
lift_comp_reindex_symm 📖	mathematical	—	LinearMap.comp PiTensorProduct DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CommSemiring.toSemiring instAddCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv RingHomInvPair.ids MultilinearMap LinearMap MultilinearMap.addCommMonoid LinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.module LinearEquiv.instEquivLike lift LinearEquiv.toLinearMap LinearEquiv.symm reindex MultilinearMap.domDomCongrLinearEquiv'	—	ext RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_self MultilinearMap.ext lift.tprod
lift_reindex 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm instAddCommMonoid instModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids MultilinearMap MultilinearMap.addCommMonoid LinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.module LinearEquiv.instEquivLike lift reindex LinearEquiv.symm MultilinearMap.domDomCongrLinearEquiv'	—	LinearMap.congr_fun RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_self lift_comp_reindex
lift_reindex_symm 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct instAddCommMonoid instModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids MultilinearMap MultilinearMap.addCommMonoid LinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike lift Equiv Equiv.instEquivLike Equiv.symm LinearEquiv.symm reindex MultilinearMap.domDomCongrLinearEquiv'	—	LinearMap.congr_fun RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_self lift_comp_reindex_symm
lift_symm 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap PiTensorProduct instAddCommMonoid instModule MultilinearMap LinearMap.addCommMonoid MultilinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MultilinearMap.instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm lift LinearMap.compMultilinearMap tprod	—	RingHomInvPair.ids smulCommClass_self
lift_tprod 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MultilinearMap PiTensorProduct instAddCommMonoid instModule LinearMap MultilinearMap.addCommMonoid LinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike lift tprod LinearMap.id	—	RingHomInvPair.ids smulCommClass_self lift.unique'
lifts_add 📖	mathematical	FreeAddMonoid Set Set.instMembership lifts	PiTensorProduct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoid AddSemigroup.toAdd AddMonoid.toAddSemigroup AddRightCancelMonoid.toAddMonoid AddCancelMonoid.toAddRightCancelMonoid FreeAddMonoid.instAddCancelMonoid	—	—
lifts_smul 📖	mathematical	FreeAddMonoid Set Set.instMembership lifts	PiTensorProduct instSMul DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddRightCancelMonoid.toAddMonoid AddCancelMonoid.toAddRightCancelMonoid FreeAddMonoid.instAddCancelMonoid AddMonoidHom.instFunLike FreeAddMonoid.map Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	mem_lifts_iff Algebra.to_smulCommClass SemigroupAction.mul_smul List.smul_sum
lifts_zero 📖	mathematical	—	FreeAddMonoid Set Set.instMembership lifts PiTensorProduct AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid AddRightCancelMonoid.toAddMonoid AddCancelMonoid.toAddRightCancelMonoid FreeAddMonoid.instAddCancelMonoid	—	mem_lifts_iff FreeAddMonoid.toList_zero
mapMonoidHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct instAddCommMonoid instModule MulOneClass.toMulOne Pi.mulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike mapMonoidHom map	—	—
mapMultilinear_apply 📖	mathematical	—	DFunLike.coe MultilinearMap LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct instAddCommMonoid instModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction instSMulCommClass MultilinearMap.instFunLikeForall mapMultilinear map	—	smulCommClass_self instSMulCommClass
map_comp 📖	mathematical	—	map LinearMap.comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids PiTensorProduct instAddCommMonoid instModule	—	ext RingHomCompTriple.ids MultilinearMap.ext map_tprod
map_comp_reindex_eq 📖	mathematical	—	LinearMap.comp PiTensorProduct DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CommSemiring.toSemiring instAddCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids map LinearEquiv.toLinearMap RingHomInvPair.ids reindex	—	ext RingHomCompTriple.ids RingHomInvPair.ids MultilinearMap.ext reindex_tprod map_tprod
map_comp_reindex_symm 📖	mathematical	—	LinearMap.comp PiTensorProduct DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CommSemiring.toSemiring instAddCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids map LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm reindex	—	ext RingHomCompTriple.ids RingHomInvPair.ids MultilinearMap.ext LinearEquiv.injective LinearEquiv.apply_symm_apply map_tprod
map_id 📖	mathematical	—	map LinearMap.id CommSemiring.toSemiring PiTensorProduct instAddCommMonoid instModule	—	ext MultilinearMap.ext map_tprod
map_mul 📖	mathematical	—	map LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.End.instMul PiTensorProduct instAddCommMonoid instModule	—	map_comp
map_one 📖	mathematical	—	map LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.End.instOne PiTensorProduct instAddCommMonoid instModule	—	map_id
map_pow 📖	mathematical	—	map Pi.instPow LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid PiTensorProduct instAddCommMonoid instModule	—	map_pow MonoidHom.instMonoidHomClass
map_range_eq_span_tprod 📖	mathematical	—	LinearMap.range PiTensorProduct CommSemiring.toSemiring instAddCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids map Submodule.span setOf DFunLike.coe MultilinearMap MultilinearMap.instFunLikeForall tprod LinearMap LinearMap.instFunLike	—	RingHomSurjective.ids Submodule.map_top span_tprod_eq_top Submodule.map_span Set.range_comp Set.ext map_tprod
map_reindex 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm instAddCommMonoid instModule LinearMap.instFunLike map LinearEquiv RingHomInvPair.ids LinearEquiv.instEquivLike reindex	—	DFunLike.congr_fun RingHomCompTriple.ids RingHomInvPair.ids map_comp_reindex_eq
map_reindex_symm 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct instAddCommMonoid instModule LinearMap.instFunLike map LinearEquiv RingHomInvPair.ids Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm LinearEquiv.instEquivLike LinearEquiv.symm reindex	—	DFunLike.congr_fun RingHomCompTriple.ids RingHomInvPair.ids map_comp_reindex_symm
map_tprod 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct instAddCommMonoid instModule LinearMap.instFunLike map MultilinearMap MultilinearMap.instFunLikeForall tprod	—	lift.tprod
map_update_add 📖	mathematical	—	map Function.update LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instAdd PiTensorProduct instAddCommMonoid instModule	—	ext MultilinearMap.ext map_tprod MultilinearMap.map_update_add
map_update_smul 📖	mathematical	—	map Function.update LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid PiTensorProduct instAddCommMonoid instModule distribMulAction' NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.to_smulCommClass Algebra.id instSMulCommClass	—	ext smulCommClass_self Algebra.to_smulCommClass instSMulCommClass MultilinearMap.ext map_tprod MultilinearMap.map_update_smul
map₂_tprod_tprod 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct instAddCommMonoid instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module instSMulCommClass map₂ MultilinearMap MultilinearMap.instFunLikeForall tprod smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self instSMulCommClass lift.tprod piTensorHomMap_tprod_tprod
mem_lifts_iff 📖	mathematical	—	FreeAddMonoid Set Set.instMembership lifts PiTensorProduct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instSMul DFunLike.coe MultilinearMap CommSemiring.toSemiring instModule MultilinearMap.instFunLikeForall tprod Equiv EquivLike.toFunLike Equiv.instEquivLike FreeAddMonoid.toList	—	FreeAddMonoid.toPiTensorProduct
nonempty_lifts 📖	mathematical	—	Set.Nonempty FreeAddMonoid lifts	—	Quot.out_eq
piTensorHomMapFun₂_add 📖	mathematical	—	piTensorHomMapFun₂ PiTensorProduct LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instSMulCommClass DistribMulAction.toDistribSMul AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoid instModule instSMulCommClass LinearMap.instAdd	—	smulCommClass_self LinearMap.instSMulCommClass instSMulCommClass ext MultilinearMap.ext map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass RingHomInvPair.ids lift.tprod
piTensorHomMapFun₂_smul 📖	mathematical	—	piTensorHomMapFun₂ PiTensorProduct LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instSMulCommClass DistribMulAction.toDistribSMul instSMul instAddCommMonoid instModule instSMulCommClass LinearMap.instSMul LinearMap.instDistribMulAction distribMulAction' NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.to_smulCommClass Algebra.id	—	smulCommClass_self LinearMap.instSMulCommClass instSMulCommClass Algebra.to_smulCommClass ext MultilinearMap.ext map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass RingHomInvPair.ids lift.tprod
piTensorHomMap_tprod_eq_map 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction instAddCommMonoid instModule instSMulCommClass LinearMap.instFunLike piTensorHomMap MultilinearMap MultilinearMap.instFunLikeForall tprod map	—	ext smulCommClass_self instSMulCommClass MultilinearMap.ext piTensorHomMap_tprod_tprod map_tprod
piTensorHomMap_tprod_tprod 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct instAddCommMonoid instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction instSMulCommClass piTensorHomMap MultilinearMap MultilinearMap.instFunLikeForall tprod	—	smulCommClass_self instSMulCommClass lift.tprod
piTensorHomMap₂_tprod_tprod_tprod 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct instAddCommMonoid instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module instSMulCommClass smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instSMulCommClass DistribMulAction.toDistribSMul piTensorHomMap₂ MultilinearMap MultilinearMap.instFunLikeForall tprod	—	smulCommClass_self instSMulCommClass LinearMap.instSMulCommClass lift.tprod piTensorHomMap_tprod_tprod
reindex_comp_tprod 📖	mathematical	—	LinearMap.compMultilinearMap PiTensorProduct DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CommSemiring.toSemiring instAddCommMonoid instModule LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids reindex tprod LinearEquiv MultilinearMap MultilinearMap.addCommMonoid MultilinearMap.instModule instSMulCommClass LinearEquiv.instEquivLike LinearEquiv.symm MultilinearMap.domDomCongrLinearEquiv'	—	MultilinearMap.ext RingHomInvPair.ids instSMulCommClass reindex_tprod
reindex_refl 📖	mathematical	—	reindex Equiv.refl LinearEquiv.refl PiTensorProduct CommSemiring.toSemiring instAddCommMonoid instModule	—	LinearEquiv.ext RingHomInvPair.ids RingHomInvPair.triples₂ instSMulCommClass CompTriple.comp_eq CompTriple.instComp_id CompTriple.instIsIdId lift_tprod LinearEquiv.ofLinear.congr_simp
reindex_reindex 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiTensorProduct Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm instAddCommMonoid instModule LinearEquiv.instEquivLike reindex Equiv.trans	—	LinearEquiv.congr_fun RingHomInvPair.ids RingHomCompTriple.ids reindex_trans
reindex_symm 📖	mathematical	—	LinearEquiv.symm PiTensorProduct CommSemiring.toSemiring instAddCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids reindex Equiv.symm	—	LinearEquiv.ext RingHomInvPair.ids Equiv.piCongrLeft'_symm RingHomInvPair.triples₂ instSMulCommClass LinearEquiv.ofLinear.congr_simp
reindex_tprod 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiTensorProduct Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm instAddCommMonoid instModule LinearEquiv.instEquivLike reindex MultilinearMap MultilinearMap.instFunLikeForall tprod	—	RingHomInvPair.ids liftAux_tprod
reindex_trans 📖	mathematical	—	LinearEquiv.trans PiTensorProduct DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CommSemiring.toSemiring instAddCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids reindex Equiv.trans	—	LinearEquiv.toLinearMap_injective RingHomInvPair.ids RingHomCompTriple.ids ext MultilinearMap.ext instSMulCommClass reindex_tprod reindex_comp_tprod
smulCommClass' 📖	mathematical	—	SMulCommClass PiTensorProduct hasSMul'	—	induction_on' SMulCommClass.smul_comm smul_add
smul_add 📖	mathematical	—	PiTensorProduct hasSMul' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoid	—	map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
smul_tprodCoeff 📖	mathematical	—	tprodCoeff Function.update	—	smul_mul_assoc one_mul smul_one_smul smul_tprodCoeff_aux
smul_tprodCoeff' 📖	mathematical	—	PiTensorProduct hasSMul' tprodCoeff SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
smul_tprodCoeff_aux 📖	mathematical	—	tprodCoeff Function.update SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Quotient.sound'
span_tprod_eq_top 📖	mathematical	—	Submodule.span PiTensorProduct CommSemiring.toSemiring instAddCommMonoid instModule Set.range DFunLike.coe MultilinearMap MultilinearMap.instFunLikeForall tprod Top.top Submodule Submodule.instTop	—	Submodule.eq_top_iff' induction_on Submodule.smul_mem Submodule.subset_span Submodule.add_mem
subsingletonEquiv_apply_tprod 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiTensorProduct instAddCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike subsingletonEquiv MultilinearMap MultilinearMap.instFunLikeForall tprod	—	lift.tprod
subsingletonEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiTensorProduct instAddCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm subsingletonEquiv MultilinearMap MultilinearMap.instFunLikeForall tprod Function.update decidableEq_of_subsingleton Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids
subsingletonEquiv_symm_apply' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiTensorProduct instAddCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm subsingletonEquiv MultilinearMap MultilinearMap.instFunLikeForall tprod	—	RingHomInvPair.ids subsingletonEquiv_apply_tprod
tmulEquivDep_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct PiTensorProduct instAddCommMonoid instModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike LinearEquiv.instEquivLike tmulEquivDep TensorProduct.tmul MultilinearMap MultilinearMap.instFunLikeForall tprod	—	RingHomInvPair.ids smulCommClass_self lift.tprod
tmulEquivDep_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiTensorProduct TensorProduct instAddCommMonoid instModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm tmulEquivDep MultilinearMap MultilinearMap.instFunLikeForall tprod TensorProduct.tmul	—	RingHomInvPair.ids lift.tprod
tmulEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct PiTensorProduct instAddCommMonoid instModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike LinearEquiv.instEquivLike tmulEquiv TensorProduct.tmul MultilinearMap MultilinearMap.instFunLikeForall tprod	—	RingHomInvPair.ids tmulEquivDep_apply
tmulEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiTensorProduct TensorProduct instAddCommMonoid instModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm tmulEquiv MultilinearMap MultilinearMap.instFunLikeForall tprod TensorProduct.tmul	—	RingHomInvPair.ids tmulEquivDep_symm_apply
tprodCoeff_eq_smul_tprod 📖	mathematical	—	tprodCoeff PiTensorProduct instSMul DFunLike.coe MultilinearMap CommSemiring.toSemiring instAddCommMonoid instModule MultilinearMap.instFunLikeForall tprod	—	mul_one
tprod_eq_tprodCoeff_one 📖	mathematical	—	DFunLike.coe MultilinearMap PiTensorProduct CommSemiring.toSemiring instAddCommMonoid instModule MultilinearMap.instFunLikeForall tprod tprodCoeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	—
zero_tprodCoeff 📖	mathematical	—	tprodCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring PiTensorProduct AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid	—	Quotient.sound'
zero_tprodCoeff' 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	tprodCoeff PiTensorProduct instAddCommMonoid	—	Quotient.sound'

PiTensorProduct.lift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tprod 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids MultilinearMap MultilinearMap.addCommMonoid LinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike PiTensorProduct.lift MultilinearMap.instFunLikeForall PiTensorProduct.tprod	—	PiTensorProduct.liftAux_tprod
unique 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule LinearMap.instFunLike MultilinearMap MultilinearMap.instFunLikeForall PiTensorProduct.tprod	LinearEquiv RingHomInvPair.ids MultilinearMap.addCommMonoid LinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike PiTensorProduct.lift	—	unique' MultilinearMap.ext
unique' 📖	mathematical	LinearMap.compMultilinearMap PiTensorProduct CommSemiring.toSemiring PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule PiTensorProduct.tprod	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MultilinearMap LinearMap MultilinearMap.addCommMonoid LinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike PiTensorProduct.lift	—	PiTensorProduct.ext RingHomInvPair.ids smulCommClass_self LinearEquiv.symm_apply_apply

PiTensorProduct.liftAux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	mathematical	—	DFunLike.coe AddMonoidHom PiTensorProduct AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid PiTensorProduct.instAddCommMonoid AddMonoidHom.instFunLike PiTensorProduct.liftAux PiTensorProduct.instSMul SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	PiTensorProduct.induction_on' Algebra.to_smulCommClass PiTensorProduct.smul_tprodCoeff' PiTensorProduct.liftAux_tprodCoeff smul_assoc IsScalarTower.left smul_add AddMonoidHom.map_add

TensorProduct

Definitions

Name	Category	Theorems
«term⨂[_]_,_» 📖	CompOp	—

---

← Back to Index