natDegree_add_le_iff_right — Mathlib

English

natDegree_add_le_iff_right: If p.natDegree ≤ n, then (p + q).natDegree ≤ n iff q.natDegree ≤ n.

Русский

Если natDegree p ≤ n, то (p+q).natDegree ≤ n эквивалентно q.natDegree ≤ n.

LaTeX

$$$p.natDegree \\le n \\Rightarrow (p + q).natDegree \\le n \\iff q.natDegree \\le n$$$

Lean4

theorem natDegree_add_le_iff_right {n : ℕ} (p q : R[X]) (pn : p.natDegree ≤ n) :
    (p + q).natDegree ≤ n ↔ q.natDegree ≤ n := by
  rw [add_comm]
  exact natDegree_add_le_iff_left _ _ pn

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