coe_X_compare — Mathlib

English

The image of the indeterminate X under ratfuncAdicComplRingEquiv K coincides with the X-embed in the power series completion.

Русский

Образ переменной X под ratfuncAdicComplRingEquiv K совпадает с образованием X в завершении степенных рядов.

LaTeX

$$$(\\mathrm{ratfuncAdicComplRingEquiv}\\,K)\\bigl(\\mathrm{RatFunc.X} : \\mathrm{RatFunc}\\,K\\bigr) = (\\mathrm{PowerSeries.X} : K\\langle\\!X\\!\\rangle)$$$

Lean4

theorem coe_X_compare :
    (ratfuncAdicComplRingEquiv K) ((RatFunc.X : RatFunc K) : RatFuncAdicCompl K) = ((PowerSeries.X : K⟦X⟧) : K⸨X⸩) :=
  by
  rw [PowerSeries.coe_X, ← RatFunc.coe_X, ← LaurentSeries_coe, ← compare_coe]
  rfl

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