Commit 2024-03-04 18:12 e3e4eeab
View on Github →feat: prove case 1 of FLT in the case n=3 (#10698)
We prove the so called case 1 of Fermat Last Theorem for exponent n = 3: if a b c : ℕ are such that ¬ 3 ∣ a * b * c then a ^ 3 + b ^ 3 ≠ c ^ 3.
From flt-regular