English
A polynomial version of FLT for three generators with a descent argument; multiplicity considerations show no nontrivial solutions exist under the three-gen setup.
Русский
Полиномная версия Фермат для трёх генераторов с нисходящим аргументом; учитывая кратность, не существует нетривиальных решений в системе трёх генераторов.
LaTeX
$$$\forall K, n\ge 3, \; a,b,c \text{ полиномы, несводимые к нулю } a^n+b^n=c^n \Rightarrow \text{нет решений}.$$$
Lean4
theorem fermatLastTheoremWith'_polynomial {n : ℕ} (hn : 3 ≤ n) (chn : (n : k) ≠ 0) : FermatLastTheoremWith' k[X] n := by
classical
rw [FermatLastTheoremWith']
intro a b c ha hb hc heq
obtain ⟨a', eq_a⟩ := gcd_dvd_left a b
obtain ⟨b', eq_b⟩ := gcd_dvd_right a b
set d := gcd a b
have hd : d ≠ 0 := gcd_ne_zero_of_left ha
rw [eq_a, eq_b, mul_pow, mul_pow, ← mul_add] at heq
have hdc : d ∣ c := by
-- TODO: This is basically reproving `IsIntegrallyClosed.pow_dvd_pow_iff`
have hn : 0 < n := by omega
have hdncn : d ^ n ∣ c ^ n := ⟨_, heq.symm⟩
simpa [dvd_iff_normalizedFactors_le_normalizedFactors, Multiset.le_iff_count, *] using hdncn
obtain ⟨c', eq_c⟩ := hdc
rw [eq_a, mul_ne_zero_iff] at ha
rw [eq_b, mul_ne_zero_iff] at hb
rw [eq_c, mul_ne_zero_iff] at hc
rw [mul_comm] at eq_a eq_b eq_c
refine ⟨d, a', b', c', ⟨eq_a, eq_b, eq_c⟩, ?_⟩
rw [eq_c, mul_pow, mul_comm, mul_left_inj' (pow_ne_zero n hd)] at heq
suffices goal : a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0
by
simp only [natDegree_eq_zero] at goal
obtain ⟨⟨ca', ha'⟩, ⟨cb', hb'⟩, ⟨cc', hc'⟩⟩ := goal
rw [← ha', ← hb', ← hc']
rw [← ha', C_ne_zero] at ha
rw [← hb', C_ne_zero] at hb
rw [← hc', C_ne_zero] at hc
exact ⟨ha.right.isUnit_C, hb.right.isUnit_C, hc.right.isUnit_C⟩
apply flt hn chn ha.right hb.right hc.right _ heq
convert isCoprime_div_gcd_div_gcd _
· exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_a.symm
· exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_b.symm
· rw [eq_b]
exact mul_ne_zero hb.right hb.left
