hasSum_mul_right_iff — Mathlib

English

For a ≠ 0, HasSum (i ↦ f i * a) (a1 * a) L iff HasSum f a1 L.

Русский

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

LaTeX

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

Lean4

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

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