powers_zero

Mathlib.RingTheory.HahnSeries.Summable

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

← MathLib Explorer

English

The powers construction of the zero Hahn series yields the constant one power: powers(0) = single 0 1.

Русский

Пусть powers применяется к нулевой серии; тогда powers(0) = single 0 1.

LaTeX

$$ $\text{powers}(0) = \text{single } 0 1 $$$

Lean4

@[simp]
theorem powers_zero : powers (0 : HahnSeries Γ R) = .single 0 1 :=
  by
  ext n
  rw [powers_of_orderTop_pos (by simp)]
  obtain rfl | ha := eq_or_ne n 0 <;> simp [*]

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

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

Разделы

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

Аффилиация

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