Mathlib v3 is deprecated. Go to Mathlib v4

Def tensor_product.neg.aux

Modification history

2020-12-11 01:46
src/linear_algebra/tensor_product.lean
chore(linear_algebra/tensor_product): Relax the ring requirement to semiring for the group instance (#5305)
Added tensor_product.neg.auxView on Github →