reverse_mul_X_pow

Mathlib.Algebra.Polynomial.Reverse

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem reverse_mul_X_pow (p : R[X]) (n : ℕ) : reverse (p * X ^ n) = reverse p := by
  induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ← mul_assoc, reverse_mul_X, ih]

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

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

Разделы

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

Аффилиация

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