Theorems · Theorem · field theory

Polynomial.isCoprime_of_is_root_of_eval_derivative_ne_zero

∀ {K : Type u_1} [inst : Field K] (f : Polynomial K) (a : K),
  Polynomial.eval a (Polynomial.derivative f) ≠ 0 →
    IsCoprime (Polynomial.X - Polynomial.C a) (f /ₘ (Polynomial.X - Polynomial.C a))

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).

Defined in

Mathlib.Algebra.Polynomial.FieldDivision

Cited by

0 results in Mathlib

Foundations

Depth 127 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Field