English
Assume G has cancellation on addition. For f in k[G], x in G, and r in k with the nonzerodivisor condition y r = 0 implies y = 0, the support of f * single x r is the image of the support of f under the right-translation by x.
Русский
Пусть G обладает свойством отмены сложения. Для f в k[G], элемента x∈G и скаляра r∈k, удовлетворяющего условию ненулевых делителей, справедливо: supp( f * single x r ) = map(addRightEmbedding x)( supp(f) ).
LaTeX
$$$\\operatorname{supp}( f * \\mathrm{single}(x,r) ) = \\operatorname{map}( \\mathrm{addRightEmbedding}(x) )( \\operatorname{supp}(f) )$$$
Lean4
theorem support_mul_single [Add G] [IsRightCancelAdd G] (f : k[G]) (r : k) (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
(f * single x r : k[G]).support = f.support.map (addRightEmbedding x) :=
MonoidAlgebra.support_mul_single (G := Multiplicative G) _ _ hr _
