X_mul_C

Mathlib.Algebra.Polynomial.Basic

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

← MathLib Explorer

English

For any r ∈ R and n, p X^n C(r) = p C(r) X^n.

Русский

Для любого r ∈ R и n: p X^n C(r) = p C(r) X^n.

LaTeX

$$$ p X^n C(r) = p C(r) X^n $$$

Lean4

/-- Prefer putting constants to the left of `X`.

This lemma is the loop-avoiding `simp` version of `Polynomial.X_mul`. -/
@[simp]
theorem X_mul_C (r : R) : X * C r = C r * X :=
  X_mul

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

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

Разделы

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

Аффилиация

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