English
For x ∈ MonoidAlgebra R G, r ∈ R, g ∈ G, the product with the basis element corresponding to g with coefficient r shifts the argument by g⁻¹ on the left: (x * single g r)(h) = x(h g⁻¹) r.
Русский
Для x ∈ MonoidAlgebra R G, r ∈ R, g ∈ G произведение с базисным элементом, соответствующим g и коэффициентом r, сдвигает аргумент слева на g⁻¹: (x * single g r)(h) = x(h g⁻¹) r.
LaTeX
$$$\\forall x \\in \\mathrm{MonoidAlgebra}(R,G), \\forall r \\in R, \\forall g,h \\in G,\\ (x * \\mathrm{single}\\, g\\, r)(h) = x(h \\cdot g^{-1}) \\cdot r.$$$
Lean4
@[to_additive (attr := simp) (dont_translate := R) mul_single_apply]
theorem mul_single_apply (x : MonoidAlgebra R G) (r : R) (g h : G) : (x * single g r) h = x (h * g⁻¹) * r :=
mul_single_apply_aux <| by simp [eq_mul_inv_iff_mul_eq]
