commute_X

Mathlib.Algebra.Polynomial.Basic

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

English

The indeterminate X commutes with any polynomial p: X p = p X.

Русский

Неопределённый X коммутирует с любым полиномом p: X p = p X.

LaTeX

$$X p = p X$$

Lean4

theorem commute_X (p : R[X]) : Commute X p :=
  X_mul

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

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

Разделы

Аффилиация

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