hsum_single

Mathlib.RingTheory.HahnSeries.Summable

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

← MathLib Explorer

English

The hsum of a single-term summable family is the term itself.

Русский

Сумма по Хану одиночного элемента равна этому элементу.

LaTeX

$$$(\\text{single } i x).hsum = x$$$

Lean4

@[simp]
theorem hsum_single {ι} [DecidableEq ι] (i : ι) (x : HahnSeries Γ R) : (single i x).hsum = x :=
  by
  ext g
  rw [coeff_hsum, finsum_eq_single _ i, single_toFun, Pi.single_eq_same]
  simp +contextual

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

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

Разделы

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

Аффилиация

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