English
If the coefficient r is left-regular with respect to the multiplication by elements of G, then the support of (single x r) * f equals the image of f.support under x·.
Русский
Если коэффициент r слева регулярен относительно умножения на элементы G, то опора (single x r) * f совпадает с образом опоры f по действию x·.
LaTeX
$$Supp( (single x r) * f ) = image (λ y. x*y) f.support$$
Lean4
theorem support_single_mul_eq_image [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k}
(hr : ∀ y, r * y = 0 ↔ y = 0) {x : G} (lx : IsLeftRegular x) :
(single x r * f : MonoidAlgebra 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 grind
simp only [mul_apply, mem_support_iff.mp yf, hr, mem_support_iff, sum_single_index, Finsupp.sum_ite_eq', Ne,
not_false_iff, if_true, zero_mul, ite_self, sum_zero, lx.eq_iff]
