English
If p ≠ 0, then deg(divX p) < deg p.
Русский
Если p ≠ 0, то deg(divX p) < deg p.
LaTeX
$$$p \\neq 0 \\Rightarrow \\operatorname{deg}(\\operatorname{divX} p) < \\operatorname{deg}(p)$$$
Lean4
theorem degree_divX_lt (hp0 : p ≠ 0) : (divX p).degree < p.degree :=
by
haveI := Nontrivial.of_polynomial_ne hp0
calc
degree (divX p) < (divX p * X + C (p.coeff 0)).degree :=
if h : degree p ≤ 0 then
by
have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]
exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))
else by
have hXp0 : divX p ≠ 0 := by simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
have : degree (C (p.coeff 0)) < degree (divX p * X) :=
calc
degree (C (p.coeff 0)) ≤ 0 := degree_C_le
_ < 1 := by decide
_ = degree (X : R[X]) := degree_X.symm
_ ≤ degree (divX p * X) := by
rw [← zero_add (degree X), degree_mul' this]
exact
add_le_add
(by
rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
exact fun h0 => h (h0.symm ▸ degree_C_le))
le_rfl
rw [degree_add_eq_left_of_degree_lt this]; exact degree_lt_degree_mul_X hXp0
_ = degree p := congr_arg _ (divX_mul_X_add _)
