English
Let f be a polynomial over a field K and a ∈ K with f′(a) ≠ 0. Then X − a and f /ₘ (X − C a) are coprime in K[X].
Русский
Пусть f — многочлен над полем K и a ∈ K с f′(a) ≠ 0. Тогда X − a и f /ₘ (X − C a) взаимно просты в K[X].
LaTeX
$$$\operatorname{IsCoprime}\bigl(X - C a : K[X],\ f /ₘ (X - C a)\bigr).$$$
Lean4
/-- If `f` is a polynomial over a field, and `a : K` satisfies `f' a ≠ 0`,
then `f / (X - a)` is coprime with `X - a`.
Note that we do not assume `f a = 0`, because `f / (X - a) = (f - f a) / (X - a)`. -/
theorem isCoprime_of_is_root_of_eval_derivative_ne_zero {K : Type*} [Field K] (f : K[X]) (a : K)
(hf' : f.derivative.eval a ≠ 0) : IsCoprime (X - C a : K[X]) (f /ₘ (X - C a)) := by
classical
refine
Or.resolve_left
(EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
(irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a)))
?_
contrapose! hf' with h
have : X - C a ∣ derivative f := X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic f h
rw [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this
rwa [← C_inj, C_0]
