mathlib

8edb3d16 - feat(representation_theory/Rep): the category of representations (#13683)

feat(representation_theory/Rep): the category of representations (#13683) We define `Rep k G`, the category of `k`-linear representations of a monoid `G`. Happily, by abstract nonsense we get that this has (co)limits and a monoidal structure for free. This should play well with the new design for representations in #13573. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>