mathlib3

fe27e720 - hom_equiv between tensor_left and ihom in category of sheaves of abelian groups