coe_one

Mathlib.RingTheory.MvPowerSeries.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.coe_one

English

The constant polynomial 1 maps to the constant power series 1 under the embedding.

Русский

Нулевая константа единицы в полиномах отображается в единичный константный степенной ряд.

LaTeX

$$$\\uparrow(1) = 1$$$

Lean4

@[simp, norm_cast]
theorem coe_one : ((1 : MvPolynomial σ R) : MvPowerSeries σ R) = 1 :=
  coe_monomial _ _

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

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

Разделы

Аффилиация

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