reverse_mul_X

Mathlib.Algebra.Polynomial.Reverse

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

← MathLib Explorer

English

For any polynomial f, reverse(f · X) = reverse(f).

Русский

Для любого многочлена f: reverse(f · X) = reverse(f).

LaTeX

$$$\operatorname{reverse}(f \cdot X) = \operatorname{reverse}(f).$$$

Lean4

@[simp]
theorem reverse_mul_X (p : R[X]) : reverse (p * X) = reverse p :=
  by
  nontriviality R
  rcases eq_or_ne p 0 with rfl | hp
  · simp
  · simp [reverse, hp]

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

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

Разделы

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

Аффилиация

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