degreeOf_neg — Mathlib

English

Same as Degrees Sub: the degree multiset of p − q is contained in the union of the degree multisets of p and q.

Русский

То же самое, что Degrees Sub: множество степеней p − q принадлежит объединению степеней p и q.

LaTeX

$$$\\mathrm{degrees}(p - q) \\leq \\mathrm{degrees}(p) \\cup \\mathrm{degrees}(q)$$$

Lean4

@[simp]
theorem degreeOf_neg (i : σ) (p : MvPolynomial σ R) : degreeOf i (-p) = degreeOf i p := by
  rw [degreeOf, degreeOf, degrees_neg]

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