mul_right

Mathlib.Topology.Algebra.InfiniteSum.Ring

URI: https://scilib.ai/kg/mathlib#HasSum.mul_right

← MathLib Explorer

English

If HasSum f a1, then HasSum (i ↦ f i * a2) (a1 * a2).

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru