reverse_neg

Mathlib.Algebra.Polynomial.Reverse

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

English

The reversal of a negated polynomial equals the negation of the reversal.

Русский

Разворот отрицательного многочлена равен отрицанию разворота.

LaTeX

$$$$\\operatorname{reverse}(-f) = -\\operatorname{reverse} f.$$$$

Lean4

@[simp]
theorem reverse_neg (f : R[X]) : reverse (-f) = -reverse f := by rw [reverse, reverse, reflect_neg, natDegree_neg]

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

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

Разделы

Аффилиация

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