Revision #1214 → #1759 · back to history
modifiedFermat's Last Theorem (statement)c825b5727fa0
| Field | From #1214 | To #1759 |
|---|
| note | FermatLastTheorem is defined as the statement that aⁿ+bⁿ=cⁿ has no nontrivial natural solution for n≥3 (statement only; the full proof is not in Mathlib). | FermatLastTheorem is defined as ∀ n ≥ 3, FermatLastTheoremFor n (the statement only; the full proof is not in Mathlib). |
modifiedCases n=1, n=2 have infinitely many solutions54286405c538
| Field | From #1214 | To #1759 |
|---|
| note | not_fermatLastTheoremFor_one/two exhibit nontrivial solutions for n=1,2 but Mathlib does not state their infinitude. | not_fermatLastTheoremFor_one and not_fermatLastTheoremFor_two exhibit nontrivial solutions for n=1,2 but Mathlib does not state their infinitude. |
modifiedPythagorean equation has infinitely many solutions52ec1de48bc3
| Field | From #1214 | To #1759 |
|---|
| note | Mathlib classifies all Pythagorean triples via a parametrization but never states the solution set is infinite. | Mathlib gives a full parametric classification of Pythagorean triples but never states the solution set is infinite. |
modifiedReduction to prime exponents6f990f1abb42
| Field | From #1214 | To #1759 |
|---|
| note | FermatLastTheorem.of_odd_primes (with FermatLastTheoremWith.mono) formalizes that proving FLT for n=4 and odd primes suffices. | FermatLastTheorem.of_odd_primes (combined with FermatLastTheoremWith.mono) formalizes that proving FLT for n=4 and odd primes suffices. |
modifiedTrivial and non-trivial solution55d5749704bc
| Field | From #1214 | To #1759 |
|---|
| note | FermatLastTheoremWith encodes non-triviality via the hypotheses a≠0,b≠0,c≠0 but there is no standalone 'trivial solution' definition. | FermatLastTheoremWith encodes non-triviality via the hypotheses a≠0, b≠0, c≠0, but there is no standalone 'trivial solution' definition. |
modifiedPythagorean theorem21d710d971e5
| Field | From #1214 | To #1759 |
|---|
| note | Mathlib proves the Pythagorean theorem in the general inner-product-space form (and an affine/Euclidean version). | Mathlib proves the Pythagorean theorem in the general inner-product-space form. |
modifiedDiophantine equatione75adb82d0f5
| Field | From #1214 | To #1759 |
|---|
| note | Mathlib defines Diophantine sets (Dioph) for Hilbert's tenth problem, but not a general 'Diophantine equation' object. | Mathlib defines Diophantine sets (Dioph) in the Hilbert-tenth-problem sense, but not a general 'Diophantine equation' object. |
modifiedFLT for n = 6, 10, 1414a6fb381bc9
| Field | From #1214 | To #1759 |
|---|
| note | FermatLastTheoremFor.mono with fermatLastTheoremThree yields n=6 (3∣6), but cases n=10,14 are unavailable since p=5,7 are not proved. | FermatLastTheoremFor.mono with fermatLastTheoremThree yields n=6 (3∣6), but n=10,14 are unavailable since p=5,7 are not proved. |