English
The scalar action distributes entrywise on the index-wise evaluation.
Русский
Действие скаляра распределяется по элементам при индексном отображении.
LaTeX
$$$ (x \cdot s) a = (of R).symm \bigl( x \cdot of R (s a) \bigr) $$$
Lean4
theorem coeff_smul {R} {V} [Semiring R] [AddCommMonoid V] [Module R V] (s : SummableFamily Γ R α)
(t : SummableFamily Γ' V β) (g : Γ') :
(smul s t).hsum.coeff g =
∑ gh ∈ VAddAntidiagonal s.isPWO_iUnion_support t.isPWO_iUnion_support g,
(s.hsum.coeff gh.1) • (t.hsum.coeff gh.2) :=
by
rw [coeff_hsum]
simp only [coeff_hsum_eq_sum, smul_toFun, HahnModule.coeff_smul, Equiv.symm_apply_apply]
simp_rw [sum_vAddAntidiagonal_eq, Finset.smul_sum, Finset.sum_smul]
rw [← sum_finsum_comm _ _ <| fun gh _ => smul_support_finite s t gh]
refine sum_congr rfl fun gh _ => ?_
rw [finsum_eq_sum _ (smul_support_finite s t gh), ← sum_product_right']
refine sum_subset (fun ab hab => ?_) (fun ab _ hab => by simp_all)
have hsupp := smul_support_subset_prod s t gh
simp_all only [mem_vaddAntidiagonal, Set.mem_iUnion, mem_support, ne_eq, Set.Finite.mem_toFinset,
Function.mem_support, Set.Finite.coe_toFinset, support_subset_iff, Set.mem_prod, Set.mem_setOf_eq, Prod.forall,
coeff_support, mem_product]
exact hsupp ab.1 ab.2 hab
