English
If NoZeroSmulDivisorsNat R holds and a polynomial f has derivative equal to zero, then natDegree(f) = 0.
Русский
При условии NoZeroSmulDivisorsNat R, если производная f равна нулю, то natDegree(f) = 0.
LaTeX
$$$\text{natDegree}(f) = 0$ if $\operatorname{derivative}(f) = 0$ and $\text{NoZeroSMulDivisors}(\mathbb{N}, R)$$$
Lean4
theorem natDegree_eq_zero_of_derivative_eq_zero [NoZeroSMulDivisors ℕ R] {f : R[X]} (h : derivative f = 0) :
f.natDegree = 0 := by
rcases eq_or_ne f 0 with (rfl | hf)
· exact natDegree_zero
rw [natDegree_eq_zero_iff_degree_le_zero]
by_contra! f_nat_degree_pos
rw [← natDegree_pos_iff_degree_pos] at f_nat_degree_pos
let m := f.natDegree - 1
have hm : m + 1 = f.natDegree := tsub_add_cancel_of_le f_nat_degree_pos
have h2 := coeff_derivative f m
rw [Polynomial.ext_iff] at h
rw [h m, coeff_zero, ← Nat.cast_add_one, ← nsmul_eq_mul', eq_comm, smul_eq_zero] at h2
replace h2 := h2.resolve_left m.succ_ne_zero
rw [hm, ← leadingCoeff, leadingCoeff_eq_zero] at h2
exact hf h2
