feat: statement of Fermat's Last Theorem (#6508)

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Oliver Nash <github@olivernash.org>

Mathlib.lean

@@ -2540,7 +2540,8 @@ import Mathlib.NumberTheory.Cyclotomic.Rat
 import Mathlib.NumberTheory.Dioph
 import Mathlib.NumberTheory.DiophantineApproximation
 import Mathlib.NumberTheory.Divisors
-import Mathlib.NumberTheory.Fermat4
+import Mathlib.NumberTheory.FLT.Basic
+import Mathlib.NumberTheory.FLT.Four
 import Mathlib.NumberTheory.FermatPsp
 import Mathlib.NumberTheory.FrobeniusNumber
 import Mathlib.NumberTheory.FunctionField

Mathlib/Data/Rat/Defs.lean

@@ -83,6 +83,8 @@ lemma num_eq_zero {q : ℚ} : q.num = 0 ↔ q = 0 := by
     exact zero_mk _ _ _
   · exact congr_arg num
 
+lemma num_ne_zero {q : ℚ} : q.num ≠ 0 ↔ q ≠ 0 := num_eq_zero.not
+
 @[simp]
 theorem divInt_eq_zero {a b : ℤ} (b0 : b ≠ 0) : a /. b = 0 ↔ a = 0 := by
   rw [←zero_divInt b, divInt_eq_iff b0 b0, zero_mul, mul_eq_zero, or_iff_left b0]

Mathlib/NumberTheory/FLT/Basic.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2023 Kevin Buzzard. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Buzzard, Yaël Dillies
+-/
+import Mathlib.Data.Nat.Parity
+import Mathlib.Data.Rat.Defs
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.TFAE
+
+/-!
+# Statement of Fermat's Last Theorem
+
+This file states the Fermat Last Theorem. We provide a statement over a general semiring with
+specific exponent, along with the usual statement over the naturals.
+-/
+
+open List
+
+/-- Statement of Fermat's Last Theorem over a given semiring with a specific exponent. -/
+def FermatLastTheoremWith (α : Type*) [Semiring α] (n : ℕ) : Prop :=
+  ∀ a b c : α, a ≠ 0 → b ≠ 0 → c ≠ 0 → a ^ n + b ^ n ≠ c ^ n
+
+/-- Statement of Fermat's Last Theorem: `a ^ n + b ^ n = c ^ n` has no nontrivial integer solution
+when `n ≥ 3`. -/
+def FermatLastTheorem : Prop := ∀ n ≥ 3, FermatLastTheoremWith ℕ n
+
+variable {α : Type*} [Semiring α] [NoZeroDivisors α] {m n : ℕ}
+
+lemma FermatLastTheoremWith.mono (hmn : m ∣ n) (hm : FermatLastTheoremWith α m) :
+    FermatLastTheoremWith α n := by
+  rintro a b c ha hb hc
+  obtain ⟨k, rfl⟩ := hmn
+  simp_rw [pow_mul']
+  refine hm _ _ _ ?_ ?_ ?_ <;> exact pow_ne_zero _ ‹_›
+
+lemma fermatLastTheoremWith_nat_int_rat_tfae (n : ℕ) :
+  TFAE [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n] := by
+  tfae_have 1 → 2
+  · rintro h a b c ha hb hc habc
+    obtain hn | hn := n.even_or_odd
+    · refine' h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
+        (Int.coe_nat_inj'.1 _)
+      push_cast
+      simp only [hn.pow_abs, habc]
+    obtain ha | ha := ha.lt_or_lt <;> obtain hb | hb := hb.lt_or_lt <;>
+      obtain hc | hc := hc.lt_or_lt
+    · refine' h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
+        (Int.coe_nat_inj'.1 _)
+      push_cast
+      simp only [abs_of_neg, neg_pow a, neg_pow b, neg_pow c, ←mul_add, habc, *]
+    · exact (by positivity : 0 < c ^ n).not_lt $ habc.symm.trans_lt $ add_neg (hn.pow_neg ha) $
+        hn.pow_neg hb
+    · refine' h b.natAbs c.natAbs a.natAbs (by positivity) (by positivity) (by positivity)
+        (Int.coe_nat_inj'.1 _)
+      push_cast
+      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, habc, add_neg_eq_iff_eq_add,
+        eq_neg_add_iff_add_eq, *]
+    · refine' h a.natAbs c.natAbs b.natAbs (by positivity) (by positivity) (by positivity)
+        (Int.coe_nat_inj'.1 _)
+      push_cast
+      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, habc, neg_add_eq_iff_eq_add,
+        eq_neg_add_iff_add_eq, *]
+    · refine' h c.natAbs a.natAbs b.natAbs (by positivity) (by positivity) (by positivity)
+        (Int.coe_nat_inj'.1 _)
+      push_cast
+      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, habc, neg_add_eq_iff_eq_add,
+        eq_add_neg_iff_add_eq, *]
+    · refine' h c.natAbs b.natAbs a.natAbs (by positivity) (by positivity) (by positivity)
+        (Int.coe_nat_inj'.1 _)
+      push_cast
+      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, habc, add_neg_eq_iff_eq_add,
+        eq_add_neg_iff_add_eq, *]
+    · exact (by positivity : 0 < a ^ n + b ^ n).not_lt $ habc.trans_lt $ hn.pow_neg hc
+    · refine' h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
+        (Int.coe_nat_inj'.1 _)
+      push_cast
+      simp only [abs_of_pos, habc, *]
+  tfae_have 2 → 3
+  · rintro h a b c ha hb hc habc
+    rw [←Rat.num_ne_zero] at ha hb hc
+    have : a.den ≠ 0 := a.den_pos.ne'
+    have : b.den ≠ 0 := b.den_pos.ne'
+    have : c.den ≠ 0 := c.den_pos.ne'
+    refine' h (a.num * b.den * c.den) (a.den * b.num * c.den) (a.den * b.den * c.num)
+      (by positivity) (by positivity) (by positivity) _
+    have : (a.den * b.den * c.den : ℚ) ^ n ≠ 0 := by positivity
+    refine' Int.cast_injective $ (div_left_inj' this).1 _
+    push_cast
+    simp only [add_div, ←div_pow, mul_div_mul_comm, div_self (by positivity : (a.den : ℚ) ≠ 0),
+      div_self (by positivity : (b.den : ℚ) ≠ 0), div_self (by positivity : (c.den : ℚ) ≠ 0),
+      one_mul, mul_one, Rat.num_div_den, habc]
+  tfae_have 3 → 1
+  · rintro h a b c
+    exact_mod_cast h a b c
+  tfae_finish

Mathlib/NumberTheory/Fermat4.lean → Mathlib/NumberTheory/FLT/Four.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Paul van Wamelen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul van Wamelen
 -/
+import Mathlib.NumberTheory.FLT.Basic
 import Mathlib.NumberTheory.PythagoreanTriples
 import Mathlib.RingTheory.Coprime.Lemmas
 import Mathlib.Tactic.LinearCombination
@@ -304,8 +305,8 @@ theorem not_fermat_42 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) : a ^ 4 + b ^
   apply Fermat42.not_minimal hf h2 hp
 #align not_fermat_42 not_fermat_42
 
-theorem not_fermat_4 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) : a ^ 4 + b ^ 4 ≠ c ^ 4 := by
-  intro heq
+theorem fermatLastTheoremFour : FermatLastTheoremWith ℤ 4 := by
+  intro a b c ha hb _ heq
   apply @not_fermat_42 _ _ (c ^ 2) ha hb
   rw [heq]; ring
-#align not_fermat_4 not_fermat_4
+#align not_fermat_4 fermatLastTheoremFour