laurent_X

Mathlib.FieldTheory.Laurent

URI: https://scilib.ai/kg/mathlib#RatFunc.laurent_X

English

The Laurent expansion sends the indeterminate X to X plus the constant Cr.

Русский

Лаурентова экспансия переводит переменную X в X плюс константу Cr.

LaTeX

$$$\\mathrm{laurent}\\_r(X) = X + C r.$$$

Lean4

@[simp]
theorem laurent_X : laurent r X = X + C r := by rw [← algebraMap_X, laurent_algebraMap, taylor_X, map_add, algebraMap_C]

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

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

Разделы

Аффилиация

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