∀ {k : Type u_4} {G : Type u_3} {H : Type u_1} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : Monoid H]
  (φ : G →* H) {A : Type u_2} [inst_3 : AddCommMonoid A] [inst_4 : Module k A] (ρ : Representation k G A),
  0 ∈ {f | ∀ (g : G) (h : H), f (φ g * h) = (ρ g) (f h)}