[Merged by Bors] - refactor(representation_theory/Rep): define `ihom` concretely

[101damnations]

---

Currently the monoidal closed instance on Rep k G is defined by transporting an instance on a functor category across a category equivalence. This was hard to work with in Lean 3 and is hard to port. This PR defines the monoidal closed instance concretely instead. Naming-wise, the explicit definition of the "internal hom" functor, the right adjoint to left-tensoring, is protected, called Rep.ihom, and then we use that to define a monoidal_closed instance, and then provide a lemma saying the resulting category_theory.ihom is Rep.ihom. Not sure this is the right approach.

[joelriou]

It looks good to me!

[semorrison]

Me too!

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests