toLaurentAlg_apply

Mathlib.Algebra.Polynomial.Laurent

URI: https://scilib.ai/kg/mathlib#Polynomial.toLaurentAlg_apply

English

The mapping to Laurent algebra applied to any polynomial f agrees with the Laurent map on f.

Русский

Отображение в алгебру Лоранта, применяемое к любому полиному f, совпадает с лорантовой картой на f.

LaTeX

$$$\\text{toLaurentAlg}(f) = \\text{toLaurent}(f)$$$

Lean4

theorem toLaurentAlg_apply [CommSemiring R] (f : R[X]) : toLaurentAlg f = toLaurent f :=
  rfl

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

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

Разделы

Аффилиация

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