totalDegree_sub — Mathlib

English

The total degree of p − q does not exceed the maximum of the total degrees of p and q.

Русский

Общая степень p − q не превосходит max(totalDegree p, totalDegree q).

LaTeX

$$$(a - b).totalDegree \\le \\max(a.totalDegree, b.totalDegree)$$$

Lean4

theorem totalDegree_sub (a b : MvPolynomial σ R) : (a - b).totalDegree ≤ max a.totalDegree b.totalDegree :=
  calc
    (a - b).totalDegree = (a + -b).totalDegree := by rw [sub_eq_add_neg]
    _ ≤ max a.totalDegree (-b).totalDegree := (totalDegree_add a (-b))
    _ = max a.totalDegree b.totalDegree := by rw [totalDegree_neg]

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