PiTensorProduct

📁 Source: Mathlib/RingTheory/PiTensorProduct.lean

Statistics

Metric	Count
Definitions PiTensorProduct, constantBaseRingEquiv, instAddCommMonoidWithOne, instAlgebra, instCommRing, instCommSemiring, instMul, instNonAssocSemiring, instNonUnitalNonAssocSemiring, instNonUnitalSemiring, instOne, instRing, instSemiring, liftAlgHom, mul, singleAlgHom, tprodMonoidHom	17
Theorems tprod, algHom_ext, algHom_ext_iff, algebraMap_apply, constantBaseRingEquiv_symm, constantBaseRingEquiv_tprod, liftAlgHom_apply, mul_assoc, mul_comm, mul_def, mul_one, mul_tprod_tprod, one_def, one_mul, singleAlgHom_apply, smul_tprod_mul_smul_tprod, tprodMonoidHom_apply, tprod_mul_tprod, tprod_noncommProd, tprod_prod, tprod	21
Total	38

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tprod 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instDistribSMul IsScalarTower Commute Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	PiTensorProduct PiTensorProduct.instMul DFunLike.coe MultilinearMap PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule MultilinearMap.instFunLikeForall PiTensorProduct.tprod	—	SemiconjBy.tprod

PiTensorProduct

Definitions

Name	Category	Theorems
constantBaseRingEquiv 📖	CompOp	3 math math: constantBaseRingEquiv_symm, constantBaseRingEquiv_tprod, dualDistribEquivOfBasis_apply_apply
instAddCommMonoidWithOne 📖	CompOp	—
instAlgebra 📖	CompOp	7 math math: liftAlgHom_apply, constantBaseRingEquiv_symm, constantBaseRingEquiv_tprod, singleAlgHom_apply, dualDistribEquivOfBasis_apply_apply, algHom_ext_iff, algebraMap_apply
instCommRing 📖	CompOp	—
instCommSemiring 📖	CompOp	1 math math: tprod_prod
instMul 📖	CompOp	5 math math: SemiconjBy.tprod, mul_def, Commute.tprod, tprod_mul_tprod, smul_tprod_mul_smul_tprod
instNonAssocSemiring 📖	CompOp	1 math math: tprodMonoidHom_apply
instNonUnitalNonAssocSemiring 📖	CompOp	—
instNonUnitalSemiring 📖	CompOp	—
instOne 📖	CompOp	1 math math: one_def
instRing 📖	CompOp	—
instSemiring 📖	CompOp	8 math math: liftAlgHom_apply, constantBaseRingEquiv_symm, constantBaseRingEquiv_tprod, singleAlgHom_apply, dualDistribEquivOfBasis_apply_apply, algHom_ext_iff, tprod_noncommProd, algebraMap_apply
liftAlgHom 📖	CompOp	1 math math: liftAlgHom_apply
mul 📖	CompOp	6 math math: mul_assoc, mul_def, one_mul, mul_one, mul_tprod_tprod, mul_comm
singleAlgHom 📖	CompOp	2 math math: singleAlgHom_apply, algHom_ext_iff
tprodMonoidHom 📖	CompOp	1 math math: tprodMonoidHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algHom_ext 📖	—	AlgHom.comp PiTensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra Algebra.id singleAlgHom	—	—	AlgHom.toLinearMap_injective ext MultilinearMap.ext MonoidHom.pi_ext DFunLike.congr_fun
algHom_ext_iff 📖	mathematical	—	AlgHom.comp PiTensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra Algebra.id singleAlgHom	—	algHom_ext
algebraMap_apply 📖	mathematical	IsScalarTower Algebra.toSMul CommSemiring.toSemiring	DFunLike.coe RingHom PiTensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring RingHom.instFunLike algebraMap instAlgebra MultilinearMap instAddCommMonoid instModule MultilinearMap.instFunLikeForall tprod Pi.mulSingle AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Algebra.algebraMap_eq_smul_one Algebra.to_smulCommClass smul_one_smul MultilinearMap.map_update_smul Function.update_eq_self isScalarTower' IsScalarTower.right Pi.one_def
constantBaseRingEquiv_symm 📖	mathematical	—	DFunLike.coe AlgEquiv PiTensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule instSemiring Algebra.id instAlgebra AlgEquiv.instFunLike AlgEquiv.symm constantBaseRingEquiv RingHom RingHom.instFunLike algebraMap	—	—
constantBaseRingEquiv_tprod 📖	mathematical	—	DFunLike.coe AlgEquiv PiTensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule instSemiring Algebra.id instAlgebra AlgEquiv.instFunLike constantBaseRingEquiv MultilinearMap instAddCommMonoid instModule MultilinearMap.instFunLikeForall tprod Finset.prod CommSemiring.toCommMonoid Finset.univ	—	lift.tprod
liftAlgHom_apply 📖	mathematical	DFunLike.coe MultilinearMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule MultilinearMap.instFunLikeForall Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	AlgHom PiTensorProduct instSemiring instAlgebra Algebra.id AlgHom.funLike liftAlgHom LinearMap RingHom.id LinearMap.instFunLike LinearEquiv instAddCommMonoid instModule MultilinearMap.addCommMonoid LinearMap.addCommMonoid MultilinearMap.instModule LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike lift	—	—
mul_assoc 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instDistribSMul IsScalarTower	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PiTensorProduct instAddCommMonoid instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module instSMulCommClass mul	—	instSMulCommClass smulCommClass_self RingHomCompTriple.ids LinearMap.instSMulCommClass SMulCommClass.symm RingHomInvPair.ids ext MultilinearMap.ext tprod_mul_tprod mul_assoc DFunLike.congr_fun
mul_comm 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule instAddCommMonoid instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module instSMulCommClass mul Algebra.to_smulCommClass IsScalarTower.right	—	instSMulCommClass Algebra.to_smulCommClass IsScalarTower.right ext MultilinearMap.ext mul_tprod_tprod mul_comm DFunLike.congr_fun
mul_def 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instDistribSMul IsScalarTower	PiTensorProduct instMul DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module instSMulCommClass mul	—	—
mul_one 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instDistribSMul IsScalarTower	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PiTensorProduct instAddCommMonoid instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module instSMulCommClass mul MultilinearMap MultilinearMap.instFunLikeForall tprod Pi.instOne AddMonoidWithOne.toOne	—	induction_on instSMulCommClass Algebra.to_smulCommClass map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass mul_tprod_tprod mul_one map_add SemilinearMapClass.toAddHomClass
mul_tprod_tprod 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instDistribSMul IsScalarTower	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PiTensorProduct instAddCommMonoid instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module instSMulCommClass mul MultilinearMap MultilinearMap.instFunLikeForall tprod Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	instSMulCommClass piTensorHomMap₂_tprod_tprod_tprod
one_def 📖	mathematical	—	PiTensorProduct AddCommMonoidWithOne.toAddCommMonoid instOne DFunLike.coe MultilinearMap CommSemiring.toSemiring instAddCommMonoid instModule MultilinearMap.instFunLikeForall tprod Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne	—	—
one_mul 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instDistribSMul IsScalarTower	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PiTensorProduct instAddCommMonoid instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module instSMulCommClass mul MultilinearMap MultilinearMap.instFunLikeForall tprod Pi.instOne AddMonoidWithOne.toOne	—	induction_on instSMulCommClass map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass mul_tprod_tprod one_mul map_add SemilinearMapClass.toAddHomClass
singleAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom PiTensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra Algebra.id AlgHom.funLike singleAlgHom MultilinearMap CommSemiring.toSemiring instAddCommMonoid instModule MultilinearMap.instFunLikeForall tprod MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Pi.mulOneClass MonoidHom.instFunLike MonoidHom.mulSingle	—	—
smul_tprod_mul_smul_tprod 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instDistribSMul IsScalarTower	PiTensorProduct instMul instSMul DFunLike.coe MultilinearMap instAddCommMonoid instModule MultilinearMap.instFunLikeForall tprod Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.instMul	—	Algebra.to_smulCommClass instSMulCommClass map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass mul_tprod_tprod mul_comm SemigroupAction.mul_smul
tprodMonoidHom_apply 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instDistribSMul IsScalarTower	DFunLike.coe MonoidHom PiTensorProduct MulOneClass.toMulOne Pi.mulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring MonoidHom.instFunLike tprodMonoidHom MultilinearMap instAddCommMonoid instModule MultilinearMap.instFunLikeForall tprod	—	—
tprod_mul_tprod 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instDistribSMul IsScalarTower	PiTensorProduct instMul DFunLike.coe MultilinearMap instAddCommMonoid instModule MultilinearMap.instFunLikeForall tprod Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_tprod_tprod
tprod_noncommProd 📖	mathematical	Set.Pairwise SetLike.coe Finset Finset.instSetLike Function.onFun Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Pi.monoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero	DFunLike.coe MultilinearMap PiTensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule CommSemiring.toSemiring instAddCommMonoid instModule MultilinearMap.instFunLikeForall tprod Finset.noncommProd instSemiring Set.Pairwise.imp Commute.tprod	—	Finset.map_noncommProd MonoidHom.instMonoidHomClass
tprod_prod 📖	mathematical	—	DFunLike.coe MultilinearMap PiTensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instAddCommMonoid instModule MultilinearMap.instFunLikeForall tprod Finset.prod Pi.commMonoid CommSemiring.toCommMonoid instCommSemiring	—	map_prod MonoidHom.instMonoidHomClass

SemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tprod 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instDistribSMul IsScalarTower SemiconjBy Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	PiTensorProduct PiTensorProduct.instMul DFunLike.coe MultilinearMap PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule MultilinearMap.instFunLikeForall PiTensorProduct.tprod	—	eq_1 PiTensorProduct.tprod_mul_tprod

(root)

Definitions

Name	Category	Theorems
PiTensorProduct 📖	CompOp	155 math math: PiTensorProduct.mapL_id, TensorAlgebra.ofDirectSum_of_tprod, PiTensorProduct.lift_reindex, PiTensorProduct.lift.tprod, PiTensorProduct.liftAlgHom_apply, PiTensorProduct.tmulEquiv_symm_apply, PiTensorProduct.mapLMonoidHom_apply, PiTensorProduct.isEmptyEquiv_apply_tprod, PiTensorProduct.dualDistribEquivOfBasis_symm_apply, FreeAddMonoid.toPiTensorProduct, PiTensorProduct.ofDirectSumEquiv_tprod_lof, PiTensorProduct.lift_reindex_symm, PiTensorProduct.map_reindex_symm, PiTensorProduct.reindex_reindex, PiTensorProduct.subsingletonEquiv_symm_apply, TensorAlgebra.toDirectSum_tensorPower_tprod, PiTensorProduct.lifts_smul, PiTensorProduct.reindex_refl, SemiconjBy.tprod, PiTensorProduct.toDualContinuousMultilinearMap_apply_apply, PiTensorProduct.mul_assoc, PiTensorProduct.map_comp, PiTensorProduct.mapL_one, PiTensorProduct.mapL_smul, PiTensorProduct.projectiveSeminorm_apply, PiTensorProduct.reindex_comp_tprod, PiTensorProduct.lifts_add, PiTensorProduct.tprod_prod, PiTensorProduct.ofFinsuppEquiv'_tprod_single, PiTensorProduct.subsingletonEquiv_apply_tprod, PiTensorProduct.constantBaseRingEquiv_symm, PiTensorProduct.projectiveSeminorm_tprod_le, PiTensorProduct.ofDirectSumEquiv_symm_lof_tprod, PiTensorProduct.tprodL_toFun, PiTensorProduct.ofFinsuppEquiv_tprod_single, PiTensorProduct.instSMulCommClass, PiTensorProduct.congr_symm_tprod, PiTensorProduct.constantBaseRingEquiv_tprod, PiTensorProduct.liftAux.smul, PiTensorProduct.mapL_coe, PiTensorProduct.ofFinsuppEquiv_symm_single_tprod, PiTensorProduct.reindex_trans, PiTensorProduct.liftIsometry_tprodL, PiTensorProduct.one_def, PiTensorProduct.injectiveSeminorm_le_projectiveSeminorm, PiTensorProduct.reindex_tprod, PiTensorProduct.tprodMonoidHom_apply, PiTensorProduct.piTensorHomMap_tprod_tprod, PiTensorProduct.lifts_zero, PiTensorProduct.norm_eval_le_injectiveSeminorm, PiTensorProduct.tprodCoeff_eq_smul_tprod, TensorPower.tprod_mul_tprod, PiTensorProduct.liftEquiv_symm_apply, PiTensorProduct.reindex_symm, PiTensorProduct.liftEquiv_apply, PiTensorProduct.liftAux_tprodCoeff, PiTensorProduct.ofDFinsuppEquiv_tprod_apply, PiTensorProduct.dualDistribInvOfBasis_apply, PiTensorProduct.mapL_mul, PiTensorProduct.zero_tprodCoeff', PiTensorProduct.mapL_comp, PiTensorProduct.piTensorHomMap_tprod_eq_map, PiTensorProduct.singleAlgHom_apply, PiTensorProduct.lift_comp_reindex, PiTensorProduct.dualDistribEquivOfBasis_apply_apply, TensorPower.multilinearMapToDual_apply_tprod, PiTensorProduct.map₂_tprod_tprod, PiTensorProduct.dualSeminorms_bounded, PiTensorProduct.map_mul, PiTensorProduct.ofFinsuppEquiv_apply, PiTensorProduct.injectiveSeminorm_apply, PiTensorProduct.map_one, PiTensorProduct.mapMultilinear_apply, PiTensorProduct.dualDistrib_apply, PiTensorProduct.smulCommClass', PiTensorProduct.ext_iff, PiTensorProduct.tprod_eq_tprodCoeff_one, PiTensorProduct.isEmptyEquiv_symm_apply, PiTensorProduct.subsingletonEquiv_symm_apply', SymmetricPower.range_mk, PiTensorProduct.piTensorHomMapFun₂_smul, PiTensorProduct.tmulEquivDep_symm_apply, PiTensorProduct.liftAux_tprod, PiTensorProduct.piTensorHomMap₂_tprod_tprod_tprod, PiTensorProduct.tmulEquivDep_apply, PiTensorProduct.algHom_ext_iff, PiTensorProduct.mul_def, PiTensorProduct.mem_lifts_iff, PiTensorProduct.ofDFinsuppEquiv_tprod_single, PiTensorProduct.map_tprod, PiTensorProduct.mapLMultilinear_apply_apply, TensorPower.list_prod_gradedMonoid_mk_single, PiTensorProduct.mapL_apply, PiTensorProduct.liftIsometry_comp_mapL, PiTensorProduct.one_mul, PiTensorProduct.liftIsometry_symm_apply, PiTensorProduct.tprod_noncommProd, PiTensorProduct.piTensorHomMapFun₂_add, PiTensorProduct.mul_one, PiTensorProduct.tmulEquiv_apply, PiTensorProduct.map_comp_reindex_symm, PiTensorProduct.smul_tprodCoeff', PiTensorProduct.mapL_opNorm, PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm, TensorPower.cast_tprod, PiTensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse, PiTensorProduct.mul_tprod_tprod, PiTensorProduct.tprodL_apply, PiTensorProduct.lift_tprod, PiTensorProduct.liftIsometry_apply_apply, TensorPower.gOne_def, PiTensorProduct.norm_eval_le_projectiveSeminorm, PiTensorProduct.lift_comp_map, PiTensorProduct.add_tprodCoeff, PiTensorProduct.isScalarTower', TensorAlgebra.mk_reindex_fin_cast, Commute.tprod, PiTensorProduct.ofFinsuppEquiv'_apply_apply, PiTensorProduct.mapL_pow, PiTensorProduct.map_reindex, TensorAlgebra.mk_reindex_cast, PiTensorProduct.mapMonoidHom_apply, PiTensorProduct.lift_comp_reindex_symm, PiTensorProduct.map_update_smul, PiTensorProduct.ofDFinsuppEquiv_symm_single_tprod, PiTensorProduct.span_tprod_eq_top, PiTensorProduct.map_comp_reindex_eq, PiTensorProduct.map_update_add, TensorAlgebra.toDirectSum_ι, PiTensorProduct.zero_tprodCoeff, PiTensorProduct.ofDirectSumEquiv_tprod_apply, PiTensorProduct.injectiveSeminorm_tprod_le, Basis.piTensorProduct_repr_tprod_apply, PiTensorProduct.mapL_add, PiTensorProduct.mul_comm, exteriorPower.toTensorPower_apply_ιMulti, PiTensorProduct.map_pow, PiTensorProduct.tprod_mul_tprod, PiTensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse, PiTensorProduct.algebraMap_apply, PiTensorProduct.smul_add, PiTensorProduct.smul_tprod_mul_smul_tprod, PiTensorProduct.mapLMultilinear_opNorm, TensorPower.toTensorAlgebra_tprod, Basis.piTensorProduct_apply, PiTensorProduct.congr_tprod, PiTensorProduct.map_range_eq_span_tprod, PiTensorProduct.add_tprodCoeff', PiTensorProduct.instIsScalarTower, PiTensorProduct.map_id, PiTensorProduct.injectiveSeminorm_def, PiTensorProduct.mapLMultilinear_toFun_apply, TensorPower.pairingDual_tprod_tprod, PiTensorProduct.tprodL_coe, PiTensorProduct.lift_symm

---

← Back to Index