natDegree_sub_le_iff_left — Mathlib

English

If q.natDegree ≤ n, then (p − q).natDegree ≤ n iff p.natDegree ≤ n.

Русский

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

LaTeX

$$$\operatorname{natDegree}(p - q) ≤ n \iff \operatorname{natDegree}(p) ≤ n$ при $\operatorname{natDegree}(q) ≤ n$$$

Lean4

theorem natDegree_sub_le_iff_left (qn : q.natDegree ≤ n) : (p - q).natDegree ≤ n ↔ p.natDegree ≤ n :=
  by
  rw [← natDegree_neg] at qn
  rw [sub_eq_add_neg, natDegree_add_le_iff_left _ _ qn]

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