X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic

English

Let f be a polynomial over a field K and a an element of K. If (X − a) divides f after dividing by the monic X − a, i.e. (X − a) | f /ₘ (X − a), then (X − a) divides the derivative f′.

Русский

Пусть f — многочлен над полем K и a ∈ K. Если (X − a) делит f после деления на (X − a) мономическим, то (X − a) делит производную f′.

LaTeX

$$$\text{If } f \in K[X], a \in K,\text{ and } (X- C a) \mid f /_{m} (X- C a),\text{ then } X- C a \mid f'.$$$

Lean4

theorem X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic {K : Type*} [Field K] (f : K[X]) {a : K}
    (hf : (X - C a) ∣ f /ₘ (X - C a)) : X - C a ∣ derivative f :=
  by
  have key := divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative f a
  have ⟨u, hu⟩ := hf
  rw [← key, hu, ← mul_add (X - C a) u _]
  use (u + derivative ((X - C a) * u))

Похожие утверждения