English
For f,g in SkewMonoidAlgebra and x in G, and a finite set s of pairs, if s encodes exactly those pairs (p1,p2) with p1·p2 = x, then (f*g).coeff x equals the finite sum over s of f.coeff p1 · p1•g.coeff p2.
Русский
Для f,g в SkewMonoidAlgebra и x в G, множество Finset s пары; если s кодирует ровно те пары (p1,p2) такие что p1·p2 = x, то (f*g).coeff x равен конечной сумме по s: f.coeff p1 · p1•g.coeff p2.
LaTeX
$$$ (f * g).\mathrm{coeff}(x) = \sum_{p \in s} f_{p.1} \; p.1 \; \cdot g_{p.2} \, , \text{ если } p.1 \cdot p.2 = x$$$
Lean4
theorem coeff_mul_antidiagonal_of_finset (f g : SkewMonoidAlgebra k G) (x : G) (s : Finset (G × G))
(hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x) : (f * g).coeff x = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2 := by
classical
let F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
calc
(f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := coeff_mul f g x
_ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [← Finset.sum_product _ _ _]
_ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G ↦ p.1 * p.2 = x, f.coeff p.1 * p.1 • g.coeff p.2 :=
(Finset.sum_filter _ _).symm
_ = ∑ p ∈ s.filter fun p : G × G ↦ p.1 ∈ f.support ∧ p.2 ∈ g.support, f.coeff p.1 * p.1 • g.coeff p.2 :=
(Finset.sum_congr (by ext; simp [Finset.mem_filter, Finset.mem_product, hs, and_comm]) fun _ _ ↦ rfl)
_ = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2 :=
Finset.sum_subset (Finset.filter_subset _ _) fun p hps hp ↦
by
simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
by_cases h1 : f.coeff p.1 = 0 <;> simp_all
