Theorem TensorProduct.homTensorHomMap_comp_map_lcomp

Modification history

2026-09-03 07:46
Mathlib/LinearAlgebra/TensorProduct/Map.lean
feat(LinearAlgebra): dual of tensor is tensor of duals for finite projective modules (#41479) …
Added TensorProduct.homTensorHomMap_comp_map_lcompView on Github →