coeffList_neg — Mathlib

English

For a polynomial P over a ring R, the coeffList of the negation of P is the list obtained by negating each coefficient of P.

Русский

Для многочлена P над кольцом R коэффициентный список -P равен списку, получаемому путем применения знака минус ко всем коэффициентам P.

LaTeX

$$$ (-P).coeffList = P.coeffList.map (-\\cdot) $$$

Lean4

@[simp]
theorem coeffList_neg : (-P).coeffList = P.coeffList.map (-·) :=
  by
  by_cases hp : P = 0
  · rw [hp, coeffList_zero, neg_zero, coeffList_zero, List.map_nil]
  · simp [coeffList]

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