English
Let R be a nonarchimedean ring. If f: α → R sums to a and g: β → R sums to b, then the function (i, j) ↦ f(i) g(j) sums to a b.
Русский
Пусть R — неархимедово кольцо. Пусть f суммируется до a, g суммируется до b. Тогда функция (i,j) ↦ f(i) g(j) суммируется до a b.
LaTeX
$$$\\displaystyle \\text{HasSum}\\ f\\ a \\rightarrow \\text{HasSum}\\ g\\ b \\Rightarrow \\text{HasSum}\\ (i,j)\\mapsto f(i)g(j)\\ (a b)$$$
Lean4
/-- Let `R` be a nonarchimedean ring, let `f : α → R` be a function that sums to `a : R`,
and let `g : β → R` be a function that sums to `b : R`. Then `fun i : α × β ↦ f i.1 * g i.2`
sums to `a * b`. -/
theorem mul_of_nonarchimedean {f : α → R} {g : β → R} {a b : R} (hf : HasSum f a) (hg : HasSum g b) :
HasSum (fun i : α × β ↦ f i.1 * g i.2) (a * b) :=
by
rw [← hasSum_iff_hasSum_compl] at *
simp only [Function.comp_def, UniformSpace.Completion.toCompl_apply, UniformSpace.Completion.coe_mul]
exact (hf.mul hg) (hf.summable.mul_of_complete_nonarchimedean hg.summable :)
