English
Let f,g ∈ SkewMonoidAlgebra k G, x ∈ G, s a Finset of pairs with hs describing x via p.1·p.2 = x. Then (f*g).coeff x equals the Finset sum over p ∈ s of f.coeff p.1 · p.1 • g.coeff p.2.
Русский
Пусть f,g ∈ SkewMonoidAlgebra k G, x ∈ G, s — финсет пар, где hs задаёт связь p.1·p.2 = x. Тогда (f*g).coeff x равен сумме по p ∈ s от f.coeff p.1 · p.1 • g.coeff p.2.
LaTeX
$$$ (f * g).\mathrm{coeff}(x) = \sum_{p \in s} f_{p.1} \; p.1 \cdot g_{p.2} $$$
Lean4
theorem mapDomain_mul [MulSemiringAction α β] [MulSemiringAction α₂ β] [MulHomClass F α α₂] {f : F}
(x y : SkewMonoidAlgebra β α) (hf : ∀ (a : α) (x : β), a • x = (f a) • x) :
mapDomain f (x * y) = mapDomain f x * mapDomain f y :=
by
rw [mul_def, map_sum]
have :
(sum x fun a b ↦ sum y fun a₂ b₂ ↦ mapDomain (↑f) (single (a * a₂) (b * a • b₂))) =
sum (mapDomain (↑f) x) fun a₁ b₁ ↦ sum (mapDomain (↑f) y) fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂) :=
by
simp_rw [mapDomain_single, map_mul]
rw [sum_mapDomain_index (by simp) (by simp [add_mul, single_add, sum_add])]
congr
ext a b c
rw [sum_mapDomain_index (by simp) (by simp [smul_add, mul_add, single_add])]
simp_rw [hf]
convert this using 4
rw [map_sum]
