Revision #2907 → #3451 · back to history
321e49b8db7e| Field | From #2907 | To #3451 |
|---|---|---|
| mathlib.decl | — | not_fermat_42 |
| mathlib.module | — | Mathlib.NumberTheory.FLT.Four |
| note | Fermat's right-triangle theorem (congruent-number style) is not present; only the related Fermat42 infrastructure exists. | Mathlib proves not_fermat_42 (a⁴+b⁴≠c²), the equation-form equivalent, but does not state the right-triangle-area formulation. |
| status | not_formalized | partial |
fc4b506babfa833e267ecb15dd74cbc36a5c5fac38ff0118faea52bc84bf