English
Let p and q be polynomials with nonzero trailing coefficients. Then the natTrailingDegree of the product equals the sum of natTrailingDegrees: (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree.
Русский
Пусть хвостовые коэффициенты p и q не равны нулю. Тогда natTrailingDegree произведения равно сумме natTrailingDegree: (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree.
LaTeX
$$$ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree $$$
Lean4
theorem natTrailingDegree_mul' (h : p.trailingCoeff * q.trailingCoeff ≠ 0) :
(p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree :=
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])
apply natTrailingDegree_eq_of_trailingDegree_eq_some
rw [trailingDegree_mul' h, Nat.cast_withTop (natTrailingDegree p + natTrailingDegree q), WithTop.coe_add, ←
Nat.cast_withTop, ← Nat.cast_withTop, ← trailingDegree_eq_natTrailingDegree hp, ←
trailingDegree_eq_natTrailingDegree hq]
