coe_X — Mathlib

English

The indeterminate X, viewed as an element of RatFunc F, maps under the natural embedding to the Laurent series whose only nonzero coefficient is 1 at index 1.

Русский

Неопределенная переменная X, рассматриваемая как элемент RatFunc F, отображается в лорантовую серию, у которой единственный ненулевой коэффициент равен 1 при индексе 1.

LaTeX

$$$\big((X : \mathrm{RatFunc} F) : F⸨X⸩\big) = \sum_{n \in \mathbb{Z}} c_n X^n,$ where $c_1 = 1$ and $c_n = 0$ for $n \neq 1$.$$

Lean4

@[simp]
theorem coe_X : ((X : RatFunc F) : F⸨X⸩) = single 1 1 := by
  simp [← algebraMap_X, ← IsScalarTower.algebraMap_apply F[X] (RatFunc F) F⸨X⸩]

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