English
If HasSum f s and HasSum g t hold and the mixed sum ∑ i, j f(i) · g(j) is summable, then the HasSum of the product equals s · t.
Русский
Если имеют место HasSum f s и HasSum g t и суммируемость смешанной суммы ∑ i, j f(i) g(j), то сумма произведения равна s · t.
LaTeX
$$$ \text{HasSum } f s \rightarrow \text{HasSum } g t \rightarrow \text{Summable } (\lambda x: ι \times κ, f x.1 * g x.2) \rightarrow \text{HasSum } (\lambda x, f x.1 * g x.2) (s * t)$$$
Lean4
theorem mul (hf : HasSum f s) (hg : HasSum g t) (hfg : Summable fun x : ι × κ ↦ f x.1 * g x.2) :
HasSum (fun x : ι × κ ↦ f x.1 * g x.2) (s * t) :=
let ⟨_u, hu⟩ := hfg
(hf.mul_eq hg hu).symm ▸ hu
