English
In the Laurent series ring R⟦X⟧, the indeterminate X, when viewed as a power series, corresponds to the monomial of degree 1 with coefficient 1; i.e. it is the power-series representation with coefficient 1 at exponent 1 and zero elsewhere.
Русский
В кольце Лорантовых рядов R⟦X⟧ неопределённая X, рассматривая её как степенной ряд, соответствует моному степени 1 с коэффициентом 1; т.е. это представление степенного ряда, в котором коэффициент при степени 1 равен 1, а все остальные коэффициенты равны нулю.
LaTeX
$$$\text{The element }X\in R\langle\!X\!\rangle \text{ corresponds to the power series with only }X^1\text{ having coefficient }1.$$$
Lean4
theorem coe_X : ((X : R⟦X⟧) : R⸨X⸩) = single 1 1 :=
ofPowerSeries_X
