hsum_mul

Mathlib.RingTheory.HahnSeries.Summable

URI: https://scilib.ai/kg/mathlib#HahnSeries.SummableFamily.hsum_mul

← MathLib Explorer

English

The hsum of a smul action is the same as the smul of hsum with the canonical map.

Русский

Сумма через smul совпадает с суммой через каноническое отображение.

LaTeX

$$$ hsum\_smul (s) (t) = smul\_hsum (s) (t) $$$

Lean4

theorem hsum_mul (s : SummableFamily Γ R α) (t : SummableFamily Γ R β) : (mul s t).hsum = s.hsum * t.hsum :=
  by
  rw [← smul_eq_mul, mul_eq_smul]
  exact smul_hsum s t

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

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

Разделы

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

Аффилиация

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