Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-11 01:46 8817c3ea

View on Github →

chore(linear_algebra/tensor_product): Relax the ring requirement to semiring for the group instance (#5305)

Estimated changes

Modified src/linear_algebra/tensor_product.lean

modified theorem linear_map.map_neg₂

added def tensor_product.neg.aux

added theorem tensor_product.neg.aux_of

modified theorem tensor_product.neg_tmul