Fermat's Last Theorem for polynomials over a field

This file states and proves the Fermat's Last Theorem for polynomials over a field. For n ≥ 3 not divisible by the characteristic of the coefficient field k and (pairwise) nonzero coprime polynomials a, b, c (over a field) with a ^ n + b ^ n = c ^ n, all polynomials must be constants.

More generally, we can prove non-solvability of the Fermat-Catalan equation: there are no non-constant polynomial solutions to the equation u * a ^ p + v * b ^ q + w * c ^ r = 0, where p, q, r ≥ 3 with p * q + q * r + r * p ≤ p * q * r , p, q, r not divisible by char k, and u, v, w are nonzero elements in k. FLT is the special case where p = q = r = n, u = v = 1, and w = -1.

The proof uses the Mason-Stothers theorem (Polynomial ABC theorem) and infinite descent (in the characteristic p case).

theorem Polynomial.flt_catalan {k : Type u_1} [Field k] [DecidableEq k] {p q r : ℕ} (hp : 0 < p) (hq : 0 < q) (hr : 0 < r) (hineq : q * r + r * p + p * q ≤ p * q * r) (chp : ↑p ≠ 0) (chq : ↑q ≠ 0) (chr : ↑r ≠ 0) {a b c : Polynomial k} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) {u v w : k} (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0) (heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0) : a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0

Nonsolvability of the Fermat-Catalan equation.

theorem Polynomial.flt {k : Type u_1} [Field k] [DecidableEq k] {n : ℕ} (hn : 3 ≤ n) (chn : ↑n ≠ 0) {a b c : Polynomial k} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) (heq : a ^ n + b ^ n = c ^ n) : a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0

theorem fermatLastTheoremWith'_polynomial {k : Type u_1} [Field k] [DecidableEq k] {n : ℕ} (hn : 3 ≤ n) (chn : ↑n ≠ 0) : FermatLastTheoremWith' (Polynomial k) n