English
If x is left-regular and the right-regular condition holds, the support of (f) * (single x r) is the image of f.support under multiplication by x.
Русский
Если x является леворегулярным и выполняются праворегулярные условия, опора f * (single x r) равна образу опоры f под умножением на x.
LaTeX
$$$(f * single\\ x\\ r).\\operatorname{support} = \\mathrm{image} (\\lambda y. y * x)\\ f.\\operatorname{support}$$$
Lean4
theorem support_single_mul_eq_image {r : k} {x : G} (lx : IsLeftRegular x) (hrx : ∀ y, r * x • y = 0 ↔ y = 0) :
(single x r * f : SkewMonoidAlgebra k G).support = Finset.image (x * ·) f.support :=
by
refine subset_antisymm (support_single_mul_subset f _ _) fun y hy ↦ ?_
obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ x * a = y := by simpa only [Finset.mem_image, exists_prop] using hy
simp [coeff_mul, mem_support_iff.mp yf, hrx, mem_support_iff, sum_single_index, Ne, zero_mul, ite_self, sum_zero,
lx.eq_iff]
