Commit 2023-03-01 07:31 7b9199f9

View on Github →

feat: port LinearAlgebra.TensorProduct (#2539) It was quite smooth. I didn't have to make changes that I expect to change downstream files, so I left few porting notes. Comments that I didn't make into porting notes:

  • attribute [local ext] ext had to be changed to attribute [local ext high] ext
  • Sometimes M ⊗ N needed to be replaced by M ⊗[R] N in theorem statements.
  • I needed to make a few fixes in other files. I want to go through the library globally and fix this error, but I'm waiting on #1881 to get merged, because those two things would have many merge conflicts.

Estimated changes

added theorem LinearMap.ltensor_add
added theorem LinearMap.ltensor_comp
added theorem LinearMap.ltensor_id
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
added theorem LinearMap.rtensor_add
added theorem LinearMap.rtensor_comp
added theorem LinearMap.rtensor_id
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
added inductive TensorProduct.Eqv
added theorem TensorProduct.add_tmul
added theorem TensorProduct.ext'
added theorem TensorProduct.ext
added theorem TensorProduct.ite_tmul
added theorem TensorProduct.lid_tmul
added theorem TensorProduct.lift_mk
added theorem TensorProduct.map_comp
added theorem TensorProduct.map_id
added theorem TensorProduct.map_mul
added theorem TensorProduct.map_one
added theorem TensorProduct.map_tmul
added def TensorProduct.mk
added theorem TensorProduct.mk_apply
added theorem TensorProduct.neg_tmul
added theorem TensorProduct.rid_tmul
added theorem TensorProduct.sub_tmul
added theorem TensorProduct.sum_tmul
added theorem TensorProduct.tmul_add
added theorem TensorProduct.tmul_ite
added theorem TensorProduct.tmul_neg
added theorem TensorProduct.tmul_sub
added theorem TensorProduct.tmul_sum
added def TensorProduct