homogenize_neg — Mathlib

English

For any polynomial p over a commutative ring, homogenize(-p) equals -(homogenize p).

Русский

Для любого многочлена p над коммутативной кольцевой структурой имеет место \\operatorname{homogenize}(-p) = -(\\operatorname{homogenize} p).

LaTeX

$$$(-p)^{\\mathrm{hom}}_n = -(p^{\\mathrm{hom}}_n).$$$

Lean4

@[simp]
theorem homogenize_neg (p : R[X]) (n : ℕ) : (-p).homogenize n = -p.homogenize n :=
  map_neg (homogenizeLM n) p

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