reflect_neg — Mathlib

English

Negation commutes with reversal: reversing the negation of a polynomial equals the negation of the reversal.

Русский

Отрицание переносится через разворот: развёртывание отрицания многочлена равно отрицанию разворота.

LaTeX

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

Lean4

@[simp]
theorem reflect_neg (f : R[X]) (N : ℕ) : reflect N (-f) = -reflect N f := by
  rw [neg_eq_neg_one_mul, ← C_1, ← C_neg, reflect_C_mul, C_neg, C_1, ← neg_eq_neg_one_mul]

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