mul_of_nonarchimedean — Mathlib

English

If f,g are summable in a nonarchimedean ring, then the product of their sums equals the sum of products over pairs: (∑ f) (∑ g) = ∑_{i,j} f(i) g(j).

Русский

Если f и g суммируемы в неархимедовом кольце, то произведение сумм равно сумме по парам: (∑ f)(∑ g) = ∑_{i,j} f(i) g(j).

LaTeX

$$$\\displaystyle \\bigl( \\sum_i f(i) \\bigr) \\cdot \\bigl( \\sum_j g(j) \\bigr) = \\sum_{i,j} f(i) g(j)$$$

Lean4

/-- Let `R` be a nonarchimedean ring. If functions `f : α → R` and `g : β → R` are summable, then
so is `fun i : α × β ↦ f i.1 * g i.2`. -/
theorem mul_of_nonarchimedean {f : α → R} {g : β → R} (hf : Summable f) (hg : Summable g) :
    Summable (fun i : α × β ↦ f i.1 * g i.2) :=
  (hf.hasSum.mul_of_nonarchimedean hg.hasSum).summable

Похожие утверждения