comp — Mathlib

English

If p and q are monic and q.natDegree ≠ 0, then p.comp q is monic.

Русский

Если p и q моничны и q.natDegree ≠ 0, то p.comp q моничен.

LaTeX

$$$p\text{ Monic} \land q\text{ Monic} \land q.natDegree \neq 0 \Rightarrow (p.comp q)\text{ Monic}.$$$

Lean4

theorem comp (hp : p.Monic) (hq : q.Monic) (h : q.natDegree ≠ 0) : (p.comp q).Monic :=
  by
  nontriviality R
  have : (p.comp q).natDegree = p.natDegree * q.natDegree :=
    natDegree_comp_eq_of_mul_ne_zero <| by simp [hp.leadingCoeff, hq.leadingCoeff]
  rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff, hq.leadingCoeff,
    one_pow, mul_one]

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