mathlib

03da6818 - feat(representation_theory): fdRep k G, the category of finite dim representations of G (#13740)

feat(representation_theory): fdRep k G, the category of finite dim representations of G (#13740) We verify that this inherits the rigid monoidal structure from `FinVect G` when `G` is a group. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>