English
Assume G is cancellative on addition. For f in k[G], x in G, and r in k with the nonzero-divisor property r*y = 0 iff y = 0, the support of single x r * f equals the image of f's support under the left-translation embedding by x.
Русский
Пусть G удовлетворяет условию отмены сложения. Для f в k[G], элемента x ∈ G и коэффициента r ∈ k, тогда supp(single x r * f) = map(addLeftEmbedding x)( supp(f) ), при условии ненулевых делителей.
LaTeX
$$$\\operatorname{supp}( \\mathrm{single}(x,r) * f ) = \\operatorname{map}( \\mathrm{addLeftEmbedding}(x) )( \\operatorname{supp}(f) )$$$
Lean4
theorem support_single_mul [Add G] [IsLeftCancelAdd G] (f : k[G]) (r : k) (hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
(single x r * f : k[G]).support = f.support.map (addLeftEmbedding x) :=
MonoidAlgebra.support_single_mul (G := Multiplicative G) _ _ hr _
