add_right — Mathlib

English

If p is monic of degree n and q.natDegree < n, then p+q is monic of degree n.

Русский

Если p мономичен степени n и q.natDegree < n, то p+q мономичен степени n.

LaTeX

$$$IsMonicOfDegree(p, n) \\land q.natDegree < n \\Rightarrow IsMonicOfDegree(p + q, n)$$$

Lean4

theorem add_right {p q : R[X]} {n : ℕ} (hp : IsMonicOfDegree p n) (hq : q.natDegree < n) : IsMonicOfDegree (p + q) n :=
  by
  rcases subsingleton_or_nontrivial R with H | H
  · simpa using hp
  refine (isMonicOfDegree_iff ..).mpr ⟨?_, ?_⟩
  · exact natDegree_add_le_of_degree_le hp.natDegree_eq.le hq.le
  · rw [coeff_add_eq_left_of_lt hq]
    exact ((isMonicOfDegree_iff p n).mp hp).2

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