∀ {k G : Type u_1} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Fintype G] {X : FDRep k G} (v : ↑X.V)
  (x x_1 : G → k), ∑ s, (x + x_1) s • (X.ρ s⁻¹) v = ∑ s, x s • (X.ρ s⁻¹) v + ∑ s, x_1 s • (X.ρ s⁻¹) v