Fermat Last Theorem in the case n = 3

The goal of this file is to prove Fermat Last theorem in the case n = 3.

Main results

• fermatLastTheoremThree_case_1: the first case of Fermat Last Theorem when n = 3: if a b c : ℕ are such that ¬ 3 ∣ a * b * c, then a ^ 3 + b ^ 3 ≠ c ^ 3.

TODO

Prove case 2.

theorem fermatLastTheoremThree_case_1 {a : ℕ} {b : ℕ} {c : ℕ} (hdvd : ¬3 ∣ a * b * c) : a ^ 3 + b ^ 3 ≠ c ^ 3

If a b c : ℕ are such that ¬ 3 ∣ a * b * c, then a ^ 3 + b ^ 3 ≠ c ^ 3.