Theorem fermatLastTheoremWith'_nat_int_tfae

Modification history

2024-09-10 11:35
Mathlib/NumberTheory/FLT/Basic.lean
feat(FermatLastTheorem): Add a relaxed variant of FLT allowing nonzero unit solutions (#16060) …
Added fermatLastTheoremWith'_nat_int_tfaeView on Github →