coeff_single_mul — Mathlib

English

For f,g ∈ SkewMonoidAlgebra k G and y ∈ G, there is an explicit expression for (f * single a r).coeff y in terms of f and a,r, and the inversion in the monoid.

Русский

Для f,g ∈ SkewMonoidAlgebra k G и y ∈ G имеется явное выражение для (f * single a r).coeff y через f, a, r и инверсию в моноиде.

LaTeX

$$$ (f * \mathrm{single}\; a\; r).\mathrm{coeff}(y) = f.sum (\lambda a' b', \; (b' \; a' \cdot) \; g_{?}) \;$$$

Lean4

@[simp]
theorem coeff_single_mul (r : k) (x : G) (f : SkewMonoidAlgebra k G) (y : G) :
    (single x r * f).coeff y = r * x • f.coeff (x⁻¹ * y) :=
  f.coeff_single_mul_aux fun _z ↦ eq_inv_mul_iff_mul_eq.symm

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