Commit 2024-04-25 15:18 fe59037a

View on Github →

feat(LinearAlgebra/TensorProduct/Basic): add LinearEquiv.(l|r)Tensor (#11731)

add LinearMap.(l|r)Tensor and their properties
add congr_symm, congr_refl_refl, congr_trans, congr_mul, congr_pow and congr_zpow

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

added theorem LinearEquiv.coe_lTensor

added theorem LinearEquiv.coe_lTensor_symm

added theorem LinearEquiv.coe_rTensor

added theorem LinearEquiv.coe_rTensor_symm

added theorem LinearEquiv.comm_trans_lTensor_trans_comm_eq

added theorem LinearEquiv.comm_trans_rTensor_trans_comm_eq

added theorem LinearEquiv.congr_trans_lTensor

added theorem LinearEquiv.congr_trans_rTensor

added def LinearEquiv.lTensor

added theorem LinearEquiv.lTensor_mul

added theorem LinearEquiv.lTensor_pow

added theorem LinearEquiv.lTensor_refl

added theorem LinearEquiv.lTensor_refl_apply

added theorem LinearEquiv.lTensor_symm_tmul

added theorem LinearEquiv.lTensor_tmul

added theorem LinearEquiv.lTensor_trans

added theorem LinearEquiv.lTensor_trans_apply

added theorem LinearEquiv.lTensor_trans_congr

added theorem LinearEquiv.lTensor_trans_rTensor

added theorem LinearEquiv.lTensor_zpow

added def LinearEquiv.rTensor

added theorem LinearEquiv.rTensor_mul

added theorem LinearEquiv.rTensor_pow

added theorem LinearEquiv.rTensor_refl

added theorem LinearEquiv.rTensor_refl_apply

added theorem LinearEquiv.rTensor_symm_tmul

added theorem LinearEquiv.rTensor_tmul

added theorem LinearEquiv.rTensor_trans

added theorem LinearEquiv.rTensor_trans_apply

added theorem LinearEquiv.rTensor_trans_congr

added theorem LinearEquiv.rTensor_trans_lTensor

added theorem LinearEquiv.rTensor_zpow

added theorem TensorProduct.congr_mul

added theorem TensorProduct.congr_pow

added theorem TensorProduct.congr_refl_refl

added theorem TensorProduct.congr_symm

added theorem TensorProduct.congr_trans

added theorem TensorProduct.congr_zpow

Modified scripts/style-exceptions.txt