coeff_succ_C

Mathlib.RingTheory.PowerSeries.Basic

URI: https://scilib.ai/kg/mathlib#PowerSeries.coeff_succ_C

English

For all a and n, coeff (n+1) (C a) = 0.

Русский

Для любых a и n, coeff (n+1) (C a) = 0.

LaTeX

$$$$ \operatorname{coeff}_{n+1}(C(a)) = 0 $$$$

Lean4

@[simp]
theorem coeff_succ_C {a : R} {n : ℕ} : coeff (n + 1) (C a) = 0 :=
  coeff_ne_zero_C n.succ_ne_zero

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

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

Разделы

Аффилиация

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