Statement of Fermat's Last Theorem

This file states Fermat's Last Theorem. We provide a statement over a general semiring with specific exponent, along with the usual statement over the naturals.

def FermatLastTheoremWith (α : Type u_1) [Semiring α] (n : ℕ) : Prop

Statement of Fermat's Last Theorem over a given semiring with a specific exponent.

Equations

• FermatLastTheoremWith α n = ∀ (a b c : α), a ≠ 0 → b ≠ 0 → c ≠ 0 → a ^ n + b ^ n ≠ c ^ n

def FermatLastTheorem : Prop

Statement of Fermat's Last Theorem: a ^ n + b ^ n = c ^ n has no nontrivial integer solution when n ≥ 3.

Equations

• FermatLastTheorem = ∀ (n : ℕ), n ≥ 3 → FermatLastTheoremWith ℕ n

theorem FermatLastTheoremWith.mono {α : Type u_1} [Semiring α] [NoZeroDivisors α] {m : ℕ} {n : ℕ} (hmn : m ∣ n) (hm : FermatLastTheoremWith α m) : FermatLastTheoremWith α n

theorem fermatLastTheoremWith_nat_int_rat_tfae (n : ℕ) : List.TFAE [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n]