English
If n ≠ 0, and p is monic of degree m, q is monic of degree n, then p ∘ q is monic of degree m·n.
Русский
Если n ≠ 0, p мономичен степени m, q мономичен степени n, то p ∘ q мономичен степени m·n.
LaTeX
$$$hn : n \\neq 0 \\\\land IsMonicOfDegree(p, m) \\\\land IsMonicOfDegree(q, n) \\\\Rightarrow IsMonicOfDegree(p \\circ q, m \\cdot n)$$$
Lean4
theorem comp {p q : R[X]} {m n : ℕ} (hn : n ≠ 0) (hp : IsMonicOfDegree p m) (hq : IsMonicOfDegree q n) :
IsMonicOfDegree (p.comp q) (m * n) :=
by
rcases subsingleton_or_nontrivial R with h | h
· simp only [isMonicOfDegree_iff_of_subsingleton, mul_eq_zero] at hp ⊢
exact .inl hp
rw [← hp.natDegree_eq, ← hq.natDegree_eq]
refine (isMonicOfDegree_iff ..).mpr ⟨natDegree_comp_le, ?_⟩
rw [coeff_comp_degree_mul_degree (hq.natDegree_eq ▸ hn), hp.leadingCoeff_eq, hq.leadingCoeff_eq, one_pow, one_mul]
