coe_X — Mathlib

English

The indeterminate X, when viewed as a polynomial, corresponds to the variable X in PowerSeries: ((X : R[X]) : PowerSeries R) = PowerSeries.X.

Русский

Переменная X, как полином, соответствует переменной X в PowerSeries: ((X : R[X]) : PowerSeries R) = PowerSeries.X.

LaTeX

$$$((X : R[X]) : PowerSeries R) = PowerSeries.X$$$

Lean4

@[simp, norm_cast]
theorem coe_X : ((X : R[X]) : PowerSeries R) = PowerSeries.X :=
  coe_monomial _ _

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