Commit 2024-09-10 11:35 b337ebd1

View on Github →

feat(FermatLastTheorem): Add a relaxed variant of FLT allowing nonzero unit solutions (#16060) Adds a variant FermatLastTheoremWith' of FLT for general commutative semirings, allowing nonzero unit solutions and their multiples.

Estimated changes

Modified Mathlib/NumberTheory/FLT/Basic.lean

added theorem FermatLastTheoremWith'.fermatLastTheoremWith

added def FermatLastTheoremWith'

added theorem FermatLastTheoremWith.fermatLastTheoremWith'

added theorem fermatLastTheoremWith'_iff_fermatLastTheoremWith

added theorem fermatLastTheoremWith'_nat_int_tfae

added theorem fermatLastTheoremWith'_of_field