coeff_C_mul

Mathlib.RingTheory.MvPowerSeries.Basic

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.coeff_C_mul

← MathLib Explorer

English

For any a ∈ R, the constant coefficient of the constant series C a equals a.

Русский

Для любого a ∈ R константный коэффициент константной серии C a равен a.

LaTeX

$$$\operatorname{coeff}(0) (C a) = a$$$

Lean4

@[simp]
theorem coeff_C_mul (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) : coeff n (C a * φ) = a * coeff n φ := by
  simpa using coeff_add_monomial_mul 0 n φ a

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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