LaurentSeries_coe

Mathlib.RingTheory.LaurentSeries

URI: https://scilib.ai/kg/mathlib#LaurentSeries.LaurentSeries_coe

English

The LaurentSeriesPkg K coe map is the same as the natural inclusion into K⟨X⟩.

Русский

Ко-векторное отображение LaurentSeriesPkg(K) совпадает с естественным включением в K⟨X⟩.

LaTeX

$$$(\mathrm{LaurentSeriesPkg}(K)).\mathrm{coe} \, x = (x: K\langle X\rangle).$$$

Lean4

@[simp]
theorem LaurentSeries_coe (x : RatFunc K) : (LaurentSeriesPkg K).coe x = (x : K⸨X⸩) :=
  rfl

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

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

Разделы

Аффилиация

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