Commit 2024-05-15 19:02 e852701e

View on Github →

feat(Mathlib.NumberTheory.FLT.Three): add FermatLastTheoremForThree_of_FermatLastTheoremThreeGen (#12767) We add FermatLastTheoremForThree_of_FermatLastTheoremThreeGen: o prove FermatLastTheoremFor 3, it is enough to prove FermatLastTheoremForThreeGen. Here FermatLastTheoremForThreeGen is more general than FermatLastTheoremFor 3, but it is needed to make a descent argument working. From the flt3 project at LFTCM2024.

Estimated changes

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

added theorem IsPrimitiveRoot.toInteger_sub_one_dvd_prime'

added theorem IsPrimitiveRoot.toInteger_sub_one_dvd_prime

Modified Mathlib/NumberTheory/FLT/Three.lean

added def FermatLastTheoremForThreeGen

added theorem FermatLastTheoremForThree_of_FermatLastTheoremThreeGen