reverse_X_pow_mul

Mathlib.Algebra.Polynomial.Reverse

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

English

For any p and n, reverse(X^n · p) = reverse(p).

Русский

Для любого p и n: reverse(X^n · p) = reverse(p).

LaTeX

$$$\operatorname{reverse}(X^{n} \cdot p) = \operatorname{reverse}(p).$$$

Lean4

@[simp]
theorem reverse_X_pow_mul (p : R[X]) (n : ℕ) : reverse (X ^ n * p) = reverse p := by
  rw [commute_X_pow p, reverse_mul_X_pow]

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

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

Разделы

Аффилиация

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