mul_apply_left — Mathlib

English

The product of two basis expansions x and y is given by a convolution: (x * y) g = ∑_{h} x(h) · y(h⁻¹ g).

Русский

Произведение двух линейных комбинаций даёт свёртку: (x * y) g = ∑_{h} x(h) · y(h⁻¹ g).

LaTeX

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

Lean4

@[to_additive (dont_translate := R) mul_apply_left]
theorem mul_apply_left (x y : MonoidAlgebra R G) (g : G) : (x * y) g = x.sum fun h r ↦ r * y (h⁻¹ * g) := by
  classical
  rw [mul_apply]
  dsimp [Finsupp.sum]
  congr! 1
  simp +contextual [← eq_inv_mul_iff_mul_eq]

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