English
From a three-gen FLT, one derives a FLT result in a cyclotomic extension, showing consistency across frameworks.
Русский
Из трёхгенераторного FLT следует результат для циклотомического расширения, согласованный с базовой теорией.
LaTeX
$$$\text{FLT}_{3\text{Gen}} \Rightarrow \text{FLT}_{3} $$$
Lean4
/-- To prove `FermatLastTheoremFor 3`, it is enough to prove `FermatLastTheoremForThreeGen`. -/
theorem FermatLastTheoremForThree_of_FermatLastTheoremThreeGen [NumberField K] [IsCyclotomicExtension { 3 } ℚ K] :
FermatLastTheoremForThreeGen hζ → FermatLastTheoremFor 3 :=
by
intro H
refine fermatLastTheoremThree_of_three_dvd_only_c (fun a b c hc ha hb ⟨x, hx⟩ hcoprime h ↦ ?_)
refine H a b c 1 (by simp [hc]) (fun hdvd ↦ ha ?_) (fun hdvd ↦ hb ?_) ?_ ?_ ?_
·
rwa [← Ideal.norm_dvd_iff (hζ.prime_norm_toInteger_sub_one_of_prime_ne_two' (by decide)),
hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)] at hdvd
·
rwa [← Ideal.norm_dvd_iff (hζ.prime_norm_toInteger_sub_one_of_prime_ne_two' (by decide)),
hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)] at hdvd
· exact dvd_trans hζ.toInteger_sub_one_dvd_prime' ⟨x, by simp [hx]⟩
· rw [show a = algebraMap _ (𝓞 K) a by simp, show b = algebraMap _ (𝓞 K) b by simp]
exact hcoprime.map _
· simp only [Units.val_one, one_mul]
exact_mod_cast h
