English
If a polynomial p ∈ R[X] has positive degree, then the degree of its derivative is exactly one less: deg(derivative p) = natDegree(p) − 1.
Русский
Если p ∈ R[X] имеет положительную степень, то deg(derivative p) = natDegree(p) − 1.
LaTeX
$$$$ \deg(\operatorname{derivative}(p)) = \operatorname{natDegree}(p) - 1 \quad\text{given } 0 < \operatorname{natDegree}(p) $$$$
Lean4
@[simp]
theorem degree_derivative_eq [NoZeroSMulDivisors ℕ R] (p : R[X]) (hp : 0 < natDegree p) :
degree (derivative p) = (natDegree p - 1 : ℕ) :=
by
apply le_antisymm
· rw [derivative_apply]
apply le_trans (degree_sum_le _ _) (Finset.sup_le _)
intro n hn
apply le_trans (degree_C_mul_X_pow_le _ _) (WithBot.coe_le_coe.2 (tsub_le_tsub_right _ _))
apply le_natDegree_of_mem_supp _ hn
· refine le_sup ?_
rw [mem_support_derivative, tsub_add_cancel_of_le, mem_support_iff]
· rw [coeff_natDegree, Ne, leadingCoeff_eq_zero]
intro h
rw [h, natDegree_zero] at hp
exact hp.false
exact hp
