English
To prove FermatLastTheoremWith in a commutative semiring with a domain, it suffices to prove it for coprime triples: If every nonzero triple with gcd 1 avoids a^n + b^n = c^n, then FermatLastTheoremWith holds for all triples.
Русский
Чтобы доказать ФЛТ в коммутативной полукольце без нулевых делителей, достаточно рассмотреть только пары и тройки с gcd(a,b,c)=1: если для таких тройок не существует равенства, то ФЛТ выполняется для всех троек.
LaTeX
$$$\\forall n\\in \\mathbb{N},\\forall R\\ [CommSemiring R] [IsDomain R],\\ (\\forall a,b,c\\in R, a,b,c\\neq 0 \\land (\\{a,b,c\\} \\text{ на } R).gcd\\ id = 1 \\Rightarrow a^n + b^n \\neq c^n)\\Rightarrow FermatLastTheoremWith R n$$$
Lean4
/-- To prove Fermat Last Theorem in any semiring that is a `NormalizedGCDMonoid` one can assume
that the `gcd` of `{a, b, c}` is `1`. -/
theorem fermatLastTheoremWith_of_fermatLastTheoremWith_coprime {n : ℕ} {R : Type*} [CommSemiring R] [IsDomain R]
[DecidableEq R] [NormalizedGCDMonoid R]
(hn : ∀ a b c : R, a ≠ 0 → b ≠ 0 → c ≠ 0 → ({ a, b, c } : Finset R).gcd id = 1 → a ^ n + b ^ n ≠ c ^ n) :
FermatLastTheoremWith R n := by
intro a b c ha hb hc habc
let s : Finset R := { a, b, c }; let d := s.gcd id
obtain ⟨A, hA⟩ : d ∣ a := gcd_dvd (by simp [s])
obtain ⟨B, hB⟩ : d ∣ b := gcd_dvd (by simp [s])
obtain ⟨C, hC⟩ : d ∣ c := gcd_dvd (by simp [s])
simp only [hA, hB, hC, mul_ne_zero_iff, mul_pow] at ha hb hc habc
rw [← mul_add, mul_right_inj' (pow_ne_zero n ha.1)] at habc
refine hn A B C ha.2 hb.2 hc.2 ?_ habc
rw [← Finset.normalize_gcd, normalize_eq_one]
obtain ⟨u, hu⟩ := normalize_associated d
refine ⟨u, mul_left_cancel₀ (mt normalize_eq_zero.mp ha.1) (hu.symm ▸ ?_)⟩
rw [← Finset.gcd_mul_left, gcd_eq_gcd_image, image_insert, image_insert, image_singleton, id_eq, id_eq, id_eq, ← hA, ←
hB, ← hC]
