smul_const — Mathlib

English

If f is Summable and g is Summable and the mixed product f i • g j is Summable, then the product of the sums equals the sum of the products.

Русский

Если f и g суммируемы и смешанное произведение f i • g j суммируемо, тогда произведение сумм равно сумме произведений.

LaTeX

$$$$ (\sum' i, f i) \; \text{smul} \; (\sum' j, g j) = \sum' z : i \times j, f z.1 \cdot g z.2. $$$$

Lean4

theorem smul_const (hf : Summable f L) (a : M) : Summable (fun z ↦ f z • a) L :=
  (hf.hasSum.smul_const _).summable

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