coeff_one

Mathlib.RingTheory.HahnSeries.Multiplication

URI: https://scilib.ai/kg/mathlib#HahnSeries.coeff_one

English

The leading coefficient of the identity Hahn series 1 is 1.

Русский

Ведущий коэффициент единичной гамильтоновой серии равен единице.

LaTeX

$$$\mathrm{leadingCoeff}(1) = 1$$$

Lean4

@[simp]
theorem coeff_one [Zero R] [One R] {a : Γ} : (1 : HahnSeries Γ R).coeff a = if a = 0 then 1 else 0 :=
  coeff_single

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

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

Разделы

Аффилиация

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