coeff_ne_zero_C

Mathlib.RingTheory.PowerSeries.Basic

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

English

If n ≠ 0, then coeff n (C a) = 0.

Русский

Если n ≠ 0, то coeff n (C a) = 0.

LaTeX

$$$$ \text{If } n \neq 0: \quad \operatorname{coeff}_n(C(a)) = 0 $$$$

Lean4

theorem coeff_ne_zero_C {a : R} {n : ℕ} (h : n ≠ 0) : coeff n (C a) = 0 := by rw [coeff_C, if_neg h]

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

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

Разделы

Аффилиация

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