const_smul — Mathlib

English

If HasSum f s with respect to L, then for any b in a monoid, HasSum (b • f) (b • s).

Русский

Если HasSum f s по L, тогда HasSum (b • f) (b • s) для любого b в моноиде.

LaTeX

$$$$ \text{HasSum } f s L \Rightarrow \text{HasSum } (\lambda i, b \cdot f i) (b \cdot s) L. $$$$

Lean4

theorem const_smul {a : α} (b : γ) (hf : HasSum f a L) : HasSum (fun i ↦ b • f i) (b • a) L :=
  hf.map (DistribMulAction.toAddMonoidHom α _) <| continuous_const_smul _

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