English
As above, the coefficient at x in f*g equals the finsum over all p in the antidiagonal set {p : G×G | p.1·p.2 = x} of f.coeff p.1 · p.1 • g.coeff p.2.
Русский
Как выше: коэффициент при x в f*g равен финсумме по всем 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
theorem coeff_mul_single_aux (f : SkewMonoidAlgebra k G) {r : k} {x y z : G} (H : ∀ a, a * x = z ↔ a = y) :
(f * single x r).coeff z = f.coeff y * y • r := by
classical
have A :
∀ a₁ b₁, ((single x r).sum fun a₂ b₂ ↦ ite (a₁ * a₂ = z) (b₁ * a₁ • b₂) 0) = ite (a₁ * x = z) (b₁ * a₁ • r) 0 :=
fun a₁ b₁ ↦ sum_single_index <| by simp
calc
(f * (single x r)).coeff z = sum f fun a b ↦ if a = y then b * y • r else 0 := by
simp [coeff_mul, A, H, sum_ite_eq']
_ = if y ∈ f.support then f.coeff y * y • r else 0 := (f.support.sum_ite_eq' _ _)
_ = f.coeff y * y • r := by split_ifs with h <;> simp [support] at h <;> simp [h]
