English
If the trailing coefficients of p and q multiply to a nonzero element, the trailing degree of the product equals the sum of trailing degrees: (p * q).trailingDegree = p.trailingDegree + q.trailingDegree.
Русский
Если произведение хвостовых коэффициентов p и q не равно нулю, то trailingDegree произведения равно сумме trailingDegree отдельных множителей.
LaTeX
$$$ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree \quad \text{provided } p.trailingCoeff \cdot q.trailingCoeff \neq 0 $$$
Lean4
theorem trailingDegree_mul' (h : p.trailingCoeff * q.trailingCoeff ≠ 0) :
(p * q).trailingDegree = p.trailingDegree + q.trailingDegree :=
by
have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])
refine le_antisymm ?_ le_trailingDegree_mul
rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq, ← ENat.coe_add]
apply trailingDegree_le_of_ne_zero
rwa [coeff_mul_natTrailingDegree_add_natTrailingDegree]
