mathlib3

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

#19170

Closed