Contraction

📁 Source: Mathlib/LinearAlgebra/Contraction.lean

Statistics

Metric	Count
Definitions contractLeft, contractRight, dualTensorHom, dualTensorHomEquiv, dualTensorHomEquivOfBasis, homTensorHomEquiv, lTensorHomEquivHomLTensor, rTensorHomEquivHomRTensor	8
Theorems comp_dualTensorHom, contractLeft_apply, contractRight_apply, dualTensorHomEquivOfBasis_apply, dualTensorHomEquivOfBasis_symm_cancel_left, dualTensorHomEquivOfBasis_symm_cancel_right, dualTensorHomEquivOfBasis_toLinearMap, dualTensorHom_apply, dualTensorHom_prodMap_zero, homTensorHomEquiv_apply, homTensorHomEquiv_toLinearMap, lTensorHomEquivHomLTensor_apply, lTensorHomEquivHomLTensor_toLinearMap, map_dualTensorHom, rTensorHomEquivHomRTensor_apply, rTensorHomEquivHomRTensor_toLinearMap, toMatrix_dualTensorHom, transpose_dualTensorHom, zero_prodMap_dualTensorHom	19
Total	27

(root)

Definitions

Name	Category	Theorems
contractLeft 📖	CompOp	9 math math: contractLeft_assoc_coevaluation, LinearMap.trace_eq_contract_of_basis', LinearMap.trace_eq_contract, LinearMap.trace_eq_contract_apply, LinearMap.trace_eq_contract', contractLeft_apply, LinearMap.trace_eq_contract_of_basis, Module.Invertible.bijective, contractLeft_assoc_coevaluation'
contractRight 📖	CompOp	1 math math: contractRight_apply
dualTensorHom 📖	CompOp	16 math math: zero_prodMap_dualTensorHom, LinearMap.trace_eq_contract, dualTensorHom_apply, LinearMap.trace_eq_contract_apply, dualTensorHomEquivOfBasis_symm_cancel_right, transpose_dualTensorHom, toMatrix_dualTensorHom, dualTensorHom_prodMap_zero, dualTensorHomEquivOfBasis_toLinearMap, dualTensorHomEquivOfBasis_symm_cancel_left, comp_dualTensorHom, map_dualTensorHom, LinearMap.trace_eq_contract_of_basis, Representation.dualTensorHom_comm, dualTensorHomEquivOfBasis_apply, FDRep.dualTensorIsoLinHom_hom_hom
dualTensorHomEquiv 📖	CompOp	1 math math: LinearMap.trace_eq_contract'
dualTensorHomEquivOfBasis 📖	CompOp	5 math math: LinearMap.trace_eq_contract_of_basis', dualTensorHomEquivOfBasis_symm_cancel_right, dualTensorHomEquivOfBasis_toLinearMap, dualTensorHomEquivOfBasis_symm_cancel_left, dualTensorHomEquivOfBasis_apply
homTensorHomEquiv 📖	CompOp	2 math math: homTensorHomEquiv_apply, homTensorHomEquiv_toLinearMap
lTensorHomEquivHomLTensor 📖	CompOp	2 math math: lTensorHomEquivHomLTensor_apply, lTensorHomEquivHomLTensor_toLinearMap
rTensorHomEquivHomRTensor 📖	CompOp	2 math math: rTensorHomEquivHomRTensor_apply, rTensorHomEquivHomRTensor_toLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_dualTensorHom 📖	mathematical	—	LinearMap.comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe LinearMap TensorProduct Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike dualTensorHom TensorProduct.tmul LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	LinearMap.ext RingHomCompTriple.ids Algebra.to_smulCommClass smulCommClass_self map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass SMulCommClass.smul_comm
contractLeft_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike contractLeft TensorProduct.tmul	—	Algebra.to_smulCommClass
contractRight_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike contractRight TensorProduct.tmul	—	Algebra.to_smulCommClass
dualTensorHomEquivOfBasis_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap TensorProduct.addCommMonoid TensorProduct.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dualTensorHomEquivOfBasis LinearMap.instFunLike dualTensorHom	—	Algebra.to_smulCommClass LinearMap.ext RingHomInvPair.ids smulCommClass_self
dualTensorHomEquivOfBasis_symm_cancel_left 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap TensorProduct Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm dualTensorHomEquivOfBasis LinearMap.instFunLike dualTensorHom	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self dualTensorHomEquivOfBasis_apply LinearEquiv.symm_apply_apply
dualTensorHomEquivOfBasis_symm_cancel_right 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike dualTensorHom LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm dualTensorHomEquivOfBasis	—	Algebra.to_smulCommClass smulCommClass_self RingHomInvPair.ids dualTensorHomEquivOfBasis_apply LinearEquiv.apply_symm_apply
dualTensorHomEquivOfBasis_toLinearMap 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap TensorProduct.addCommMonoid TensorProduct.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction dualTensorHomEquivOfBasis dualTensorHom	—	Algebra.to_smulCommClass smulCommClass_self RingHomInvPair.ids
dualTensorHom_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike TensorProduct Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction dualTensorHom TensorProduct.tmul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Algebra.to_smulCommClass smulCommClass_self
dualTensorHom_prodMap_zero 📖	mathematical	—	LinearMap.prodMap CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike dualTensorHom TensorProduct.tmul LinearMap.instZero Prod.instAddCommMonoid Prod.instModule LinearMap.comp RingHomCompTriple.ids LinearMap.fst LinearMap.inl	—	LinearMap.prod_ext Algebra.to_smulCommClass smulCommClass_self RingHomCompTriple.ids LinearMap.ext smul_zero
homTensorHomEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv homTensorHomEquiv LinearMap.instFunLike TensorProduct.homTensorHomMap	—	smulCommClass_self RingHomInvPair.ids TensorProduct.smulCommClass_left LinearEquiv.coe_toLinearMap homTensorHomEquiv_toLinearMap
homTensorHomEquiv_toLinearMap 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero homTensorHomEquiv TensorProduct.homTensorHomMap	—	TensorProduct.ext smulCommClass_self TensorProduct.smulCommClass_left RingHomInvPair.ids LinearMap.ext RingHomCompTriple.ids LinearMap.compr₂ₛₗ.congr_simp rTensorHomEquivHomRTensor_apply LinearMap.instSMulCommClass TensorProduct.lift.equiv_apply lTensorHomEquivHomLTensor_apply
lTensorHomEquivHomLTensor_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv lTensorHomEquivHomLTensor LinearMap.instFunLike TensorProduct.lTensorHomToHomLTensor	—	smulCommClass_self RingHomInvPair.ids TensorProduct.smulCommClass_left LinearEquiv.coe_toLinearMap lTensorHomEquivHomLTensor_toLinearMap
lTensorHomEquivHomLTensor_toLinearMap 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero lTensorHomEquivHomLTensor TensorProduct.lTensorHomToHomLTensor	—	RingHomInvPair.ids Algebra.to_smulCommClass smulCommClass_self LinearEquiv.surjective TensorProduct.smulCommClass_left RingHomCompTriple.ids LinearMap.cancel_right TensorProduct.ext LinearMap.ext dualTensorHomEquivOfBasis_apply dualTensorHomEquivOfBasis_symm_cancel_left TensorProduct.tmul_smul TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.left
map_dualTensorHom 📖	mathematical	—	TensorProduct.map RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearMap TensorProduct Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike dualTensorHom TensorProduct.tmul TensorProduct.dualDistrib	—	TensorProduct.ext Algebra.to_smulCommClass smulCommClass_self LinearMap.ext RingHomCompTriple.ids
rTensorHomEquivHomRTensor_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv rTensorHomEquivHomRTensor LinearMap.instFunLike TensorProduct.rTensorHomToHomRTensor	—	smulCommClass_self RingHomInvPair.ids TensorProduct.smulCommClass_left LinearEquiv.coe_toLinearMap rTensorHomEquivHomRTensor_toLinearMap
rTensorHomEquivHomRTensor_toLinearMap 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero rTensorHomEquivHomRTensor TensorProduct.rTensorHomToHomRTensor	—	RingHomInvPair.ids Algebra.to_smulCommClass smulCommClass_self LinearEquiv.surjective TensorProduct.smulCommClass_left RingHomCompTriple.ids LinearMap.cancel_right TensorProduct.ext LinearMap.ext dualTensorHomEquivOfBasis_apply dualTensorHomEquivOfBasis_symm_cancel_left
toMatrix_dualTensorHom 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix TensorProduct Module.Dual Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike dualTensorHom TensorProduct.tmul Module.Basis.coord Module.Basis Module.Basis.instFunLike Matrix.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass LinearMap.toMatrix_apply Module.Basis.repr_self Finsupp.single_eq_same one_smul Matrix.single.congr_simp Matrix.single_apply_same Finsupp.single_eq_pi_single map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finsupp.smul_single mul_one Matrix.single_apply_of_ne and_iff_not_or_not Pi.single_eq_of_ne' Pi.single.congr_simp Pi.single_eq_of_ne Pi.single_zero
transpose_dualTensorHom 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike Module.Dual.transpose TensorProduct Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule dualTensorHom TensorProduct.tmul Module.Dual.eval	—	LinearMap.ext smulCommClass_self LinearMap.instSMulCommClass Algebra.to_smulCommClass MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass mul_comm
zero_prodMap_dualTensorHom 📖	mathematical	—	LinearMap.prodMap CommSemiring.toSemiring LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instZero DFunLike.coe TensorProduct Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike dualTensorHom TensorProduct.tmul Prod.instAddCommMonoid Prod.instModule LinearMap.comp RingHomCompTriple.ids LinearMap.snd LinearMap.inr	—	LinearMap.prod_ext Algebra.to_smulCommClass smulCommClass_self RingHomCompTriple.ids LinearMap.ext smul_zero

---

← Back to Index