coeff_mul_single — Mathlib

English

For f,g ∈ SkewMonoidAlgebra k G and x ∈ G, (f*g).coeff x equals the finite sum over p ∈ {p : G×G | p.1·p.2 = x} of f.coeff p.1 · p.1 • g.coeff p.2.

Русский

Для f,g ∈ SkewMonoidAlgebra k G и x ∈ G, (f*g).coeff x равен конечной сумме по всем p ∈ {p : G×G | p.1·p.2 = x} от f.coeff p.1 · p.1 • g.coeff p.2.

LaTeX

$$$ (f * g).\mathrm{coeff}(x) = \sum_{p \in \{ p : G \times G \mid p.1 \cdot p.2 = x \}} f_{p.1} \; p.1 \cdot g_{p.2} $$$

Lean4

@[simp]
theorem coeff_mul_single (f : SkewMonoidAlgebra k G) (r : k) (x y : G) :
    (f * single x r).coeff y = f.coeff (y * x⁻¹) * (y * x⁻¹) • r :=
  f.coeff_mul_single_aux fun _a ↦ eq_mul_inv_iff_mul_eq.symm

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