coeff_single

Mathlib.RingTheory.HahnSeries.Basic

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

English

The coefficient of (single a r) at b is r if b = a, and 0 otherwise.

Русский

Коэффициент (single a r) при b равен r, если b = a, и 0 иным образом.

LaTeX

$$$(single\, a\, r).\mathrm{coeff}(b) = \begin{cases} r, & b = a \\ 0, & b \neq a \end{cases}$$$

Lean4

theorem coeff_single : (single a r).coeff b = if b = a then r else 0 := by split_ifs with h <;> simp [h]

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

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

Разделы

Аффилиация

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