mathlib

0caf3701 - feat(representation_theory/Rep): describe monoidal closed structure (#18148)

feat(representation_theory/Rep): describe monoidal closed structure (#18148) The monoidal closed structure on `Rep k G` defines an internal hom of representations; we show this agrees with `representation.lin_hom`. Moreover, the maps defining the hom-set bijection come from the tensor-hom adjunction for $k$-modules.