Commit 2023-05-22 12:09 f9055dfd

View on Github →

feat: port LinearAlgebra.Contraction (#4124)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Contraction.lean

added theorem comp_dualTensorHom

added def contractLeft

added theorem contractLeft_apply

added def contractRight

added theorem contractRight_apply

added def dualTensorHom

added theorem dualTensorHomEquivOfBasis_apply

added theorem dualTensorHomEquivOfBasis_symm_cancel_left

added theorem dualTensorHomEquivOfBasis_symm_cancel_right

added theorem dualTensorHomEquivOfBasis_toLinearMap

added theorem dualTensorHom_apply

added theorem dualTensorHom_prodMap_zero

added theorem homTensorHomEquiv_apply

added theorem homTensorHomEquiv_toLinearMap

added theorem lTensorHomEquivHomLTensor_apply

added theorem lTensorHomEquivHomLTensor_toLinearMap

added theorem map_dualTensorHom

added theorem rTensorHomEquivHomRTensor_apply

added theorem rTensorHomEquivHomRTensor_toLinearMap

added theorem toMatrix_dualTensorHom

added theorem transpose_dualTensorHom

added theorem zero_prodMap_dualTensorHom

Modified Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

Modified Mathlib/LinearAlgebra/TensorProduct.lean

added theorem LinearMap.coe_lTensorHom

deleted theorem LinearMap.coe_ltensorHom

added theorem LinearMap.coe_rTensorHom

deleted theorem LinearMap.coe_rtensorHom

added def LinearMap.lTensor

added def LinearMap.lTensorHom

added theorem LinearMap.lTensor_add

added theorem LinearMap.lTensor_comp

added theorem LinearMap.lTensor_comp_apply

added theorem LinearMap.lTensor_comp_map

added theorem LinearMap.lTensor_comp_rTensor

added theorem LinearMap.lTensor_id

added theorem LinearMap.lTensor_id_apply

added theorem LinearMap.lTensor_mul

added theorem LinearMap.lTensor_neg

added theorem LinearMap.lTensor_pow

added theorem LinearMap.lTensor_smul

added theorem LinearMap.lTensor_sub

added theorem LinearMap.lTensor_tmul

added theorem LinearMap.lTensor_zero

deleted def LinearMap.ltensor

deleted def LinearMap.ltensorHom

deleted theorem LinearMap.ltensor_add

deleted theorem LinearMap.ltensor_comp

deleted theorem LinearMap.ltensor_comp_apply

deleted theorem LinearMap.ltensor_comp_map

deleted theorem LinearMap.ltensor_comp_rtensor

deleted theorem LinearMap.ltensor_id

deleted theorem LinearMap.ltensor_id_apply

deleted theorem LinearMap.ltensor_mul

deleted theorem LinearMap.ltensor_neg

deleted theorem LinearMap.ltensor_pow

deleted theorem LinearMap.ltensor_smul

deleted theorem LinearMap.ltensor_sub

deleted theorem LinearMap.ltensor_tmul

deleted theorem LinearMap.ltensor_zero

added theorem LinearMap.map_comp_lTensor

deleted theorem LinearMap.map_comp_ltensor

added theorem LinearMap.map_comp_rTensor

deleted theorem LinearMap.map_comp_rtensor

added def LinearMap.rTensor

added def LinearMap.rTensorHom

added theorem LinearMap.rTensor_add

added theorem LinearMap.rTensor_comp

added theorem LinearMap.rTensor_comp_apply

added theorem LinearMap.rTensor_comp_lTensor

added theorem LinearMap.rTensor_comp_map

added theorem LinearMap.rTensor_id

added theorem LinearMap.rTensor_id_apply

added theorem LinearMap.rTensor_mul

added theorem LinearMap.rTensor_neg

added theorem LinearMap.rTensor_pow

added theorem LinearMap.rTensor_smul

added theorem LinearMap.rTensor_sub

added theorem LinearMap.rTensor_tmul

added theorem LinearMap.rTensor_zero

deleted def LinearMap.rtensor

deleted def LinearMap.rtensorHom

deleted theorem LinearMap.rtensor_add

deleted theorem LinearMap.rtensor_comp

deleted theorem LinearMap.rtensor_comp_apply

deleted theorem LinearMap.rtensor_comp_ltensor

deleted theorem LinearMap.rtensor_comp_map

deleted theorem LinearMap.rtensor_id

deleted theorem LinearMap.rtensor_id_apply

deleted theorem LinearMap.rtensor_mul

deleted theorem LinearMap.rtensor_neg

deleted theorem LinearMap.rtensor_pow

deleted theorem LinearMap.rtensor_smul

deleted theorem LinearMap.rtensor_sub

deleted theorem LinearMap.rtensor_tmul

deleted theorem LinearMap.rtensor_zero

added def TensorProduct.lTensorHomToHomLTensor

added theorem TensorProduct.lTensorHomToHomLTensor_apply

deleted def TensorProduct.ltensorHomToHomLtensor

deleted theorem TensorProduct.ltensorHomToHomLtensor_apply

added def TensorProduct.rTensorHomToHomRTensor

added theorem TensorProduct.rTensorHomToHomRTensor_apply

deleted def TensorProduct.rtensorHomToHomRtensor

deleted theorem TensorProduct.rtensorHomToHomRtensor_apply

Modified Mathlib/RingTheory/TensorProduct.lean

modified theorem LinearMap.baseChange_eq_ltensor

added theorem TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor

deleted theorem TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rtensor