Def TensorProduct.addMonoid

Modification history

2023-11-23 09:45

Mathlib/LinearAlgebra/TensorProduct.lean

chore(LinearAlgebra/TensorProduct): make the bad instance private (#8571) …

Deleted TensorProduct.addMonoid View on Github →

2023-03-01 07:31

Mathlib/LinearAlgebra/TensorProduct.lean

feat: port LinearAlgebra.TensorProduct (#2539) …

Added TensorProduct.addMonoid View on Github →