Def category_theory.monoidal_preadditive_of_faithful

fix(*): mark some classes as Prop (#18015)

feat(representation_theory): fdRep k G is k-linear with finite dimensional hom spaces (#13789)