coeff_single_of_ne

Mathlib.RingTheory.HahnSeries.Basic

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

English

If b ≠ a, then the coefficient of (single a r) at b is 0.

Русский

Если b ≠ a, то коэффициент (single a r) при b равен 0.

LaTeX

$$$(single\, a\, r).\mathrm{coeff}(b) = 0\quad\text{если } b \neq a$$

Lean4

@[simp]
theorem coeff_single_of_ne (h : b ≠ a) : (single a r).coeff b = 0 := by
  classical exact Pi.single_eq_of_ne (M := fun _ => R) h r

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

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

Разделы

Аффилиация

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