∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Add G] [inst_2 : DecidableEq G] (f : AddMonoidAlgebra k G)
  (r : k) (a : G), (AddMonoidAlgebra.single a r * f).support ⊆ Finset.image (fun x => a + x) f.support