coeff_mul_left — Mathlib

English

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

Русский

Для f,g ∈ SkewMonoidAlgebra k G и x ∈ G, (f*g).coeff x = ∑_{a,b} f(a) · b · a • g(b) при a⁻¹ x = ...

LaTeX

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

Lean4

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

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