natDegree_add_le_iff_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem natDegree_add_le_iff_left {n : ℕ} (p q : R[X]) (qn : q.natDegree ≤ n) :
    (p + q).natDegree ≤ n ↔ p.natDegree ≤ n :=
  by
  refine ⟨fun h => ?_, fun h => natDegree_add_le_of_degree_le h qn⟩
  refine natDegree_le_iff_coeff_eq_zero.mpr fun m hm => ?_
  convert natDegree_le_iff_coeff_eq_zero.mp h m hm using 1
  rw [coeff_add, natDegree_le_iff_coeff_eq_zero.mp qn _ hm, add_zero]

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