Mathlib v3 is deprecated. Go to Mathlib v4

Theorem tensor_product.neg.aux_of

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.aux_ofView on Github →