Pullback of representation

Stream: Is there code for X?

[Gareth Ma]

If I have variable {k G G' : Type u} [CommRing k] [Group G] [Group G'] (A : Rep k G') (φ : G →* G') then I can construct a representation of $G$ by Rep.of (A.ρ.comp φ). Is this in Mathlib, or should I define things in terms of this, or should I make this a new definition?