Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ltensor_hom_equiv_hom_ltensor_apply

Modification history

2022-05-18 20:08

src/linear_algebra/contraction.lean

feat(linear_algebra/trace): trace of tensor_products and hom_tensor_hom is an equivalence (#13728)

Added ltensor_hom_equiv_hom_ltensor_apply View on Github →