English
If p and q are monic polynomials of degrees m and n respectively, then their product pq is monic of degree m+n.
Русский
Если полиномы p и q монические степеней m и n соответственно, то произведение pq моноик и имеет степень m+n.
LaTeX
$$$ (p q) \text{ is monic of degree } (m+n)$$$
Lean4
theorem mul {p q : R[X]} {m n : ℕ} (hp : IsMonicOfDegree p m) (hq : IsMonicOfDegree q n) :
IsMonicOfDegree (p * q) (m + n) :=
by
rcases subsingleton_or_nontrivial R with H | H
· simp only [isMonicOfDegree_iff_of_subsingleton, Nat.add_eq_zero] at hp hq ⊢
exact ⟨hp, hq⟩
refine ⟨?_, hp.monic.mul hq.monic⟩
have : p.leadingCoeff * q.leadingCoeff ≠ 0 :=
by
rw [hp.leadingCoeff_eq, hq.leadingCoeff_eq, one_mul]
exact one_ne_zero
rw [natDegree_mul' this, hp.natDegree_eq, hq.natDegree_eq]
