English
If the product of leading coefficients is nonzero, then deg(p q) = deg p + deg q.
Русский
Если произведение ведущих коэффициентов не равно нулю, то deg(p q) = deg p + deg q.
LaTeX
$$deg(p q) = deg p + deg q при leadingCoeff p · leadingCoeff q ≠ 0$$
Lean4
theorem degree_mul' (h : leadingCoeff p * leadingCoeff q ≠ 0) : degree (p * q) = degree p + degree q :=
have hp : p ≠ 0 := by refine mt ?_ h; exact fun hp => by rw [hp, leadingCoeff_zero, zero_mul]
have hq : q ≠ 0 := by refine mt ?_ h; exact fun hq => by rw [hq, leadingCoeff_zero, mul_zero]
le_antisymm (degree_mul_le _ _)
(by
rw [degree_eq_natDegree hp, degree_eq_natDegree hq]
refine le_degree_of_ne_zero (n := natDegree p + natDegree q) ?_
rwa [coeff_mul_degree_add_degree])
