Mathlib v3 is deprecated. Go to Mathlib v4

Theorem dual_tensor_hom_equiv_of_basis_symm_cancel_right

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 dual_tensor_hom_equiv_of_basis_symm_cancel_rightView on Github →