coeff_mul_right — Mathlib

English

For f,g ∈ SkewMonoidAlgebra k G and x ∈ G, (f*g).coeff x equals the sum over a,b of f.coeff (x a⁻¹) · (x a⁻¹) • b.

Русский

Для f,g ∈ SkewMonoidAlgebra k G и x ∈ G, (f*g).coeff x = ∑ f_{x a⁻¹} · (x a⁻¹) · g_b.

LaTeX

$$$ (f * g).\mathrm{coeff}(x) = \sum_{a,b} f_{x a^{-1}} \; (x a^{-1}) \cdot g_{b} $$$

Lean4

theorem coeff_mul_right (f g : SkewMonoidAlgebra k G) (x : G) :
    (f * g).coeff x = g.sum fun a b ↦ f.coeff (x * a⁻¹) * (x * a⁻¹) • b :=
  calc
    (f * g).coeff x = sum g fun a b ↦ (f * single a b).coeff x := by rw [← coeff_sum, ← mul_sum f g, g.sum_single]
    _ = _ := by simp

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