coeff_zero_X_mul

Mathlib.RingTheory.PowerSeries.Basic

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

English

The constant term of X multiplied by φ is zero.

Русский

Постоянный коэффициент X умножения на φ равен нулю.

LaTeX

$$$\\forall R\\ [\\operatorname{Semiring} R],\\ \\forall \\phi \\in R\\llbracket X\\rrbracket,\\ \\operatorname{coeff}_0(X \\cdot \\phi) = 0$$$

Lean4

theorem coeff_zero_X_mul (φ : R⟦X⟧) : coeff 0 (X * φ) = 0 := by simp

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

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

Разделы

Аффилиация

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