Mathlib v3 is deprecated. Go to Mathlib v4

Def tensor_algebra.tprod

Modification history

2022-05-23 10:20

src/linear_algebra/tensor_algebra/basic.lean

feat(linear_algebra/tensor_algebra/basic): add `tensor_algebra.tprod` (#14197) …

Added tensor_algebra.tprod View on Github →