Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-21 17:48 bc3ad25a

View on Github →

feat(linear_algebra/tensor_algebra): Add missing lemmas about subtraction (#5428)

Estimated changes

Modified src/linear_algebra/tensor_product.lean

added theorem linear_map.map_sub₂

added theorem tensor_product.sub_tmul

added theorem tensor_product.tmul_sub