English
If f and g have sums s and t respectively, and the double series ∑ i, j f(i) · g(j) is summable to u, then s · t = u.
Русский
Если суммы функций f и g равны s и t соответственно, и двойная сумма по i, j от f(i) g(j) сходится к u, то s · t = u.
LaTeX
$$$ \text{HasSum } f s \rightarrow \text{HasSum } g t \rightarrow \text{HasSum } (\lambda x: ι \times κ, f x.1 * g x.2) u \rightarrow s * t = u$$$
Lean4
theorem mul_eq (hf : HasSum f s) (hg : HasSum g t) (hfg : HasSum (fun x : ι × κ ↦ f x.1 * g x.2) u) : s * t = u :=
have key₁ : HasSum (fun i ↦ f i * t) (s * t) := hf.mul_right t
have this : ∀ i : ι, HasSum (fun c : κ ↦ f i * g c) (f i * t) := fun i ↦ hg.mul_left (f i)
have key₂ : HasSum (fun i ↦ f i * t) u := HasSum.prod_fiberwise hfg this
key₁.unique key₂
