comp_X_add_C — Mathlib

English

If p is monic, then the composition with X + C r is monic for all r ∈ R.

Русский

Если p моничен, то композиция c X + C r монична для всех r ∈ R.

LaTeX

$$$p\text{ Monic} \Rightarrow \ (p.comp\ (X + C\, r))\text{ Monic}.$$$

Lean4

theorem comp_X_add_C (hp : p.Monic) (r : R) : (p.comp (X + C r)).Monic :=
  by
  nontriviality R
  refine hp.comp (monic_X_add_C _) fun ha ↦ ?_
  rw [natDegree_X_add_C] at ha
  exact one_ne_zero ha

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