hasSum_mul_left_iff — Mathlib

English

For a ≠ 0, HasSum (i ↦ a * f i) (a * a1) L if and only if HasSum f a1 L.

Русский

Для a ≠ 0, HasSum (a · f(i)) (a · a1) ⇔ HasSum f a1.

LaTeX

$$$(\forall{a_1 a_2}, a_2 \neq 0) \Rightarrow \left( HasSum (\lambda i, a_2 \cdot f(i)) (a_2 \cdot a_1) \ L \iff HasSum f a_1 L \right)$$$

Lean4

theorem hasSum_mul_left_iff (h : a₂ ≠ 0) : HasSum (fun i ↦ a₂ * f i) (a₂ * a₁) L ↔ HasSum f a₁ L :=
  ⟨fun H ↦ by simpa only [inv_mul_cancel_left₀ h] using H.mul_left a₂⁻¹, HasSum.mul_left _⟩

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