Theorem TensorProduct.Neg.aux_of

Modification history

2023-10-06 14:17

Mathlib/LinearAlgebra/TensorProduct.lean

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

Deleted TensorProduct.Neg.aux_of View on Github →

2023-03-01 07:31

Mathlib/LinearAlgebra/TensorProduct.lean

feat: port LinearAlgebra.TensorProduct (#2539) …

Added TensorProduct.Neg.aux_of View on Github →