coe_def

Mathlib.RingTheory.PowerSeries.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.coe_def

English

The polynomial φ, viewed as a power series, equals PowerSeries.mk(coeff φ).

Русский

Полином φ, рассматриваемый как ряд, равен PowerSeries.mk(coeff φ).

LaTeX

$$$\\varphi : PowerSeries R = \\PowerSeries.mk(\\operatorname{coeff}(\\varphi))$$$

Lean4

theorem coe_def : (φ : PowerSeries R) = PowerSeries.mk (coeff φ) :=
  rfl

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

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

Разделы

Аффилиация

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