natDegree_add_le — Mathlib

English

For polynomials p and q, natDegree(p+q) ≤ max(natDegree p, natDegree q).

Русский

Для многочленов p и q natDegree(p+q) ≤ max(natDegree p, natDegree q).

LaTeX

$$$ \operatorname{natDegree}(p+q) \le \max(\operatorname{natDegree}(p), \operatorname{natDegree}(q)) $$$

Lean4

theorem natDegree_add_le (p q : R[X]) : natDegree (p + q) ≤ max (natDegree p) (natDegree q) := by
  rcases le_max_iff.1 (degree_add_le p q) with h | h <;> simp [natDegree_le_natDegree h]

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