Commit 2023-03-23 22:20 0caf3701

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.