Def TensorProduct.Neg.aux

Modification history

2023-10-06 14:17

Mathlib/LinearAlgebra/TensorProduct.lean

refactor(TensorProduct): golf the definition of Neg (#7546)

Modified TensorProduct.Neg.aux View on Github →

2023-03-01 07:31

Mathlib/LinearAlgebra/TensorProduct.lean

feat: port LinearAlgebra.TensorProduct (#2539) …

Added TensorProduct.Neg.aux View on Github →