English
A broad polynomial FLT statement: for a,b,c nonzero polynomials over a field, IsCoprime(a,b) and a^n+b^n=c^n, then certain degree conditions hold or derivatives vanish.
Русский
Общее полиномное утверждение Ферма: для ненулевых полиномов a,b,c над полем, взаимно простых a,b и a^n+b^n=c^n, выполняются определённые условия по степеням или все производные равны нулю.
LaTeX
$$$\forall n\ge 3,\; a,b,c \in k[X],\; a,b,c \neq 0,\; \gcd(a,b)=1,\; a^n+b^n=c^n\Rightarrow (\text{deg-условия} \lor \text{derivatives all zero}).$$$
Lean4
theorem flt {n : ℕ} (hn : 3 ≤ n) (chn : (n : k) ≠ 0) {a b c : k[X]} (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 :=
by
have hn' : 0 < n := by linarith
rw [← sub_eq_zero, ← one_mul (a ^ n), ← one_mul (b ^ n), ← one_mul (c ^ n), sub_eq_add_neg, ← neg_mul] at heq
have hone : (1 : k[X]) = C 1 := by rfl
have hneg_one : (-1 : k[X]) = C (-1) := by simp only [map_neg, map_one]
simp_rw [hneg_one, hone] at heq
apply
flt_catalan hn'.ne' hn'.ne' hn'.ne' _ chn chn chn ha hb hc hab one_ne_zero one_ne_zero (neg_ne_zero.mpr one_ne_zero)
heq
have eq_lhs : n * n + n * n + n * n = 3 * n * n := by ring
rw [eq_lhs, mul_assoc, mul_assoc]
exact Nat.mul_le_mul_right (n * n) hn
