mul_left — Mathlib

English

If HasSum f a1 with respect to a summation filter L, then HasSum (i ↦ a2 * f(i)) (a2 * a1) with the same L.

Русский

Если ∑ f(i) = a1 (в рамках суммирования), то ∑ (a2 · f(i)) = a2 · a1.

LaTeX

$$$\text{HasSum } f\ a_1\ L \Rightarrow \text{HasSum } (\lambda i, a_2 \cdot f(i))\ (a_2 \cdot a_1)\ L$$$

Lean4

theorem mul_left (a₂) (h : HasSum f a₁ L) : HasSum (fun i ↦ a₂ * f i) (a₂ * a₁) L := by
  simpa only using h.map (AddMonoidHom.mulLeft a₂) (continuous_const.mul continuous_id)

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