English
Fermat's Last Theorem holds for n = 3: there are no nonzero integers a, b, c with a^3 + b^3 = c^3.
Русский
Теорема Ферма для n = 3: не существует не нулевых целых a, b, c таких, что a^3 + b^3 = c^3.
LaTeX
$$$a^3 + b^3 \neq c^3$ for nonzero integers a,b,c$$
Lean4
/-- Fermat's Last Theorem for `n = 3`: if `a b c : ℕ` are all non-zero then
`a ^ 3 + b ^ 3 ≠ c ^ 3`. -/
theorem fermatLastTheoremThree : FermatLastTheoremFor 3 := by
classical
let K := CyclotomicField 3 ℚ
let hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K
have : NumberField K := IsCyclotomicExtension.numberField { 3 } ℚ _
apply FermatLastTheoremForThree_of_FermatLastTheoremThreeGen hζ
intro a b c u hc ha hb hcdvd coprime H
let S' : FermatLastTheoremForThreeGen.Solution' hζ :=
{ a := a
b := b
c := c
u := u
ha := ha
hb := hb
hc := hc
coprime := coprime
hcdvd := hcdvd
H := H }
obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'
obtain ⟨Smin, hSmin⟩ := S.exists_minimal
obtain ⟨Sfin, hSfin⟩ := Smin.exists_Solution_multiplicity_lt
linarith [hSmin Sfin]
