Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-18 20:08 5fe43a91

View on Github →

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

Estimated changes

Modified src/linear_algebra/contraction.lean

added theorem dual_tensor_hom_equiv_of_basis_symm_cancel_left

added theorem dual_tensor_hom_equiv_of_basis_symm_cancel_right

added def hom_tensor_hom_equiv

added theorem hom_tensor_hom_equiv_apply

added theorem hom_tensor_hom_equiv_to_linear_map

added theorem ltensor_hom_equiv_hom_ltensor_apply

added theorem ltensor_hom_equiv_hom_ltensor_to_linear_map

added theorem map_dual_tensor_hom

added theorem rtensor_hom_equiv_hom_rtensor_apply

added theorem rtensor_hom_equiv_hom_rtensor_to_linear_map

Modified src/linear_algebra/tensor_product.lean

added def tensor_product.ltensor_hom_to_hom_ltensor

added theorem tensor_product.ltensor_hom_to_hom_ltensor_apply

added def tensor_product.rtensor_hom_to_hom_rtensor

added theorem tensor_product.rtensor_hom_to_hom_rtensor_apply

Modified src/linear_algebra/trace.lean

added theorem linear_map.trace_tensor_product'

added theorem linear_map.trace_tensor_product