degrees_sub_le — Mathlib

English

The multiset of degrees of p − q is a sub-multiset of the union of the degree multisets of p and q.

Русский

Множество степеней p − q является подподержкой объединения степеней p и q.

LaTeX

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

Lean4

theorem degrees_sub_le [DecidableEq σ] {p q : MvPolynomial σ R} : (p - q).degrees ≤ p.degrees ∪ q.degrees := by
  simpa [degrees_def] using AddMonoidAlgebra.supDegree_sub_le

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