English
General polynomial version: nonsolvability of Fermat–Catalan type equations in a broad polynomial setting with coprimality assumptions.
Русский
Обобщенная полиномная версия: недостижимость уравнений типа Фермат-Каталана в широком полиномном контексте под предположением взаимной простоты.
LaTeX
$$$\forall p,q,r>0,\; \gcd(a,b)=1 \Rightarrow a^p+b^q=c^r \text{ has no nontrivial polynomial solutions.}$$$
Lean4
/-- Nonsolvability of the Fermat-Catalan equation. -/
theorem flt_catalan {p q r : ℕ} (hp : p ≠ 0) (hq : q ≠ 0) (hr : r ≠ 0) (hineq : q * r + r * p + p * q ≤ p * q * r)
(chp : (p : k) ≠ 0) (chq : (q : k) ≠ 0) (chr : (r : k) ≠ 0) {a b c : k[X]} (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 := by
-- WLOG argument: essentially three times flt_catalan_aux
have hbc : IsCoprime b c := by apply rot_coprime heq hab <;> assumption
have heq' : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0 := by rwa [add_rotate] at heq
have hca : IsCoprime c a := by apply rot_coprime heq' hbc <;> assumption
refine ⟨?_, ?_, ?_⟩
· apply flt_catalan_aux heq <;> assumption
· rw [add_rotate] at heq hineq
rw [mul_rotate] at hineq
apply flt_catalan_aux heq <;> assumption
· rw [← add_rotate] at heq hineq
rw [← mul_rotate] at hineq
apply flt_catalan_aux heq <;> assumption
