single_mul_apply — Mathlib

English

For x ∈ MonoidAlgebra R G, r ∈ R, g ∈ G, the product with the basis element on the left yields: (single g r) * x evaluated at h equals r times x(g⁻¹ h).

Русский

Для x ∈ MonoidAlgebra R G, r ∈ R, g ∈ G произведение с базисным элементом слева дает: (single g r) * x (h) = r · x(g⁻¹ h).

LaTeX

$$$\\forall x \\in \\mathrm{MonoidAlgebra}(R,G),\\forall r\\in R,\\forall g,h\\in G,\\ (\\mathrm{single}\\, g\\, r * x)(h) = r \\cdot x(g^{-1} h).$$$

Lean4

@[to_additive (attr := simp) (dont_translate := R) single_mul_apply]
theorem single_mul_apply (x : MonoidAlgebra R G) (r : R) (g h : G) : (single g r * x) h = r * x (g⁻¹ * h) :=
  single_mul_apply_aux <| by simp [eq_inv_mul_iff_mul_eq]

Похожие утверждения