X_mul

Mathlib.Algebra.Polynomial.Basic

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

← MathLib Explorer

English

X^n commutes with any polynomial p: X^n * p = p * X^n.

Русский

X^n коммутирует с любым полином p: X^n * p = p * X^n.

LaTeX

$$$ X^n \cdot p = p \cdot X^n $$$

Lean4

/-- `X` commutes with everything, even when the coefficients are noncommutative. -/
theorem X_mul : X * p = p * X := by
  rcases p with ⟨⟩
  simp only [X, ← ofFinsupp_single, ← ofFinsupp_mul, ofFinsupp.injEq]
  ext
  simp [AddMonoidAlgebra.mul_apply, add_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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