hsum_zero

Mathlib.RingTheory.HahnSeries.Summable

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

English

The sum of the zero summable family is the zero Hahn series.

Русский

Сумма нулевой суммируемой семейства равна нулевому ряду Хана.

LaTeX

$$$ (0 : SummableFamily Γ R α).hsum = 0 $$$

Lean4

@[simp]
theorem hsum_zero : (0 : SummableFamily Γ R α).hsum = 0 :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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