add_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem add_left {p q : R[X]} {n : ℕ} (hp : p.natDegree < n) (hq : IsMonicOfDegree q n) : IsMonicOfDegree (p + q) n :=
  by
  rw [add_comm]
  exact hq.add_right hp

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