const_div — Mathlib

English

If HasSum (i ↦ 1 / f(i)) a L, then for any b, HasSum (i ↦ b / f(i)) (b * a) L.

Русский

Если сумма по 1/f(i) равна a, то сумма b/f(i) равна b a.

LaTeX

$$$\text{HasSum } (\lambda i, 1/f(i))\ a\ L \Rightarrow \forall b, \text{HasSum } (\lambda i, b/f(i))\ (b \cdot a)\ L$$$

Lean4

theorem const_div (h : HasSum (fun x ↦ 1 / f x) a L) (b : α) : HasSum (fun i ↦ b / f i) (b * a) L :=
  by
  have := h.mul_left b
  simpa only [div_eq_mul_inv, one_mul] using this

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