Mason-Stothers theorem

This file states and proves the Mason-Stothers theorem, which is a polynomial version of the ABC conjecture. For (pairwise) coprime polynomials a, b, c (over a field) with a + b + c = 0, we have max {deg(a), deg(b), deg(c)} + 1 ≤ deg(rad(abc)) or a' = b' = c' = 0.

Proof is based on this online note by Franz Lemmermeyer http://www.fen.bilkent.edu.tr/~franz/ag05/ag-02.pdf, which is essentially based on Noah Snyder's paper "An Alternative Proof of Mason's Theorem", but slightly different.

TODO

Prove polynomial FLT using Mason-Stothers theorem.

theorem Polynomial.abc {k : Type u_1} [Field k] [DecidableEq k] {a b c : Polynomial k} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) (hbc : IsCoprime b c) (hca : IsCoprime c a) (hsum : a + b + c = 0) : a.natDegree + 1 ≤ (UniqueFactorizationMonoid.radical (a * b * c)).natDegree ∧ b.natDegree + 1 ≤ (UniqueFactorizationMonoid.radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (UniqueFactorizationMonoid.radical (a * b * c)).natDegree ∨ Polynomial.derivative a = 0 ∧ Polynomial.derivative b = 0 ∧ Polynomial.derivative c = 0

Polynomial ABC theorem.