Powers of a separable minimal polynomial

Let L / K be a field extension and let x ∈ L be separable over K. Then x is a simple root of minpoly K x, so the multiplicity of x as a root of a polynomial p ∈ K[X] is the multiplicity of minpoly K x as a factor of p: minpoly K x ^ m divides p if and only if (X - x) ^ m divides p in L[X]. For m = 1 this reduces to minpoly.dvd_iff.

In Thue's method of Diophantine approximation this turns high-order vanishing of a polynomial with rational coefficients at an algebraic number α into divisibility by a power of the minimal polynomial of α, and hence into a lower bound for its degree.

Separability is needed: over a field K of characteristic p containing an element a which is not a p-th power, a p-th root x of a has minpoly K x = X ^ p - a = (X - x) ^ p, so (X - x) ^ p divides minpoly K x while minpoly K x ^ p does not.

Main results

• minpoly.pow_dvd_iff: for x separable over K, a polynomial p ∈ K[X] is divisible by minpoly K x ^ m if and only if (X - x) ^ m divides p in L[X].

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 6, Lemma 6.11.

theorem minpoly.pow_dvd_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x : L} (hx : IsSeparable K x) {p : Polynomial K} {m : ℕ} : minpoly K x ^ m ∣ p ↔ (Polynomial.X - Polynomial.C x) ^ m ∣ Polynomial.map (algebraMap K L) p

For x separable over K, a polynomial p ∈ K[X] is divisible by minpoly K x ^ m if and only if (X - x) ^ m divides p in L[X].