aeval_add — Mathlib

English

If p is monic of degree n, then for any r ∈ R, the polynomial obtained by evaluating p at X + r, i.e., aeval(X + r) p, is monic of degree n.

Русский

Если p моноичен степени n, то для любого r ∈ R многочлен aeval(X + r) p моноичен степени n.

LaTeX

$$$\\operatorname{IsMonicOfDegree}\\bigl(\\operatorname{aeval}(X + C r) p,\, n\\bigr)$$$

Lean4

theorem aeval_add {p : R[X]} {n : ℕ} (hp : IsMonicOfDegree p n) (r : R) : IsMonicOfDegree (aeval (X + C r) p) n :=
  by
  rcases subsingleton_or_nontrivial R with H | H
  · simpa using hp
  rw [← mul_one n]
  exact hp.comp one_ne_zero (isMonicOfDegree_X_add_one r)

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