Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-04 14:06 e303a7d9

View on Github →

feat(linear_algebra/tensor_product): tensoring linear maps with modules (#4771)

Estimated changes

Modified src/linear_algebra/tensor_product.lean

added theorem linear_map.coe_ltensor_hom

added theorem linear_map.coe_rtensor_hom

added def linear_map.ltensor

added theorem linear_map.ltensor_add

added theorem linear_map.ltensor_comp

added theorem linear_map.ltensor_comp_map

added theorem linear_map.ltensor_comp_rtensor

added def linear_map.ltensor_hom

added theorem linear_map.ltensor_id

added theorem linear_map.ltensor_neg

added theorem linear_map.ltensor_smul

added theorem linear_map.ltensor_sub

added theorem linear_map.ltensor_tmul

added theorem linear_map.ltensor_zero

added theorem linear_map.map_comp_ltensor

added theorem linear_map.map_comp_rtensor

added def linear_map.rtensor

added theorem linear_map.rtensor_add

added theorem linear_map.rtensor_comp

added theorem linear_map.rtensor_comp_ltensor

added theorem linear_map.rtensor_comp_map

added def linear_map.rtensor_hom

added theorem linear_map.rtensor_id

added theorem linear_map.rtensor_neg

added theorem linear_map.rtensor_smul

added theorem linear_map.rtensor_sub

added theorem linear_map.rtensor_tmul

added theorem linear_map.rtensor_zero