Commit 2024-03-28 10:26 f9c49c90

View on Github →

feat(LinearAlgebra/DirectSum/Finsupp): add some more variants of finsuppTensorFinsupp (#11598)

add finsuppTensorFinsuppLid, finsuppTensorFinsuppRid as well as their simp lemmas
make finsuppTensorFinsupp' a special case of finsuppTensorFinsuppLid
add TensorProduct.lid_eq_rid

Estimated changes

Modified Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

added theorem finsuppTensorFinsupp'_symm_single_eq_single_one_tmul

added theorem finsuppTensorFinsupp'_symm_single_eq_tmul_single_one

added theorem finsuppTensorFinsupp'_symm_single_mul

added def finsuppTensorFinsuppLid

added theorem finsuppTensorFinsuppLid_apply_apply

added theorem finsuppTensorFinsuppLid_self

added theorem finsuppTensorFinsuppLid_single_tmul_single

added theorem finsuppTensorFinsuppLid_symm_single_smul

added def finsuppTensorFinsuppRid

added theorem finsuppTensorFinsuppRid_apply_apply

added theorem finsuppTensorFinsuppRid_self

added theorem finsuppTensorFinsuppRid_single_tmul_single

added theorem finsuppTensorFinsuppRid_symm_single_smul

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

added theorem TensorProduct.lid_eq_rid