Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-29 03:48 8edb3d16

View on Github →

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.

Estimated changes