natDegree_add_le_of_degree_le — Mathlib

English

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

Русский

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

LaTeX

$$$ \operatorname{natDegree}(p+q) \le n \text{, если } \operatorname{natDegree}(p) \le n \text{ и } \operatorname{natDegree}(q) \le n $$$

Lean4

theorem natDegree_add_le_of_degree_le {p q : R[X]} {n : ℕ} (hp : natDegree p ≤ n) (hq : natDegree q ≤ n) :
    natDegree (p + q) ≤ n :=
  (natDegree_add_le p q).trans <| max_le hp hq

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