Commit 2023-09-12 12:40 ca73a84a

View on Github →

feat: statement of Fermat's Last Theorem (#6508)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Rat/Defs.lean

added theorem Rat.num_ne_zero

Created Mathlib/NumberTheory/FLT/Basic.lean

added def FermatLastTheorem

added theorem FermatLastTheoremWith.mono

added def FermatLastTheoremWith

added theorem fermatLastTheoremWith_nat_int_rat_tfae

Renamed Mathlib/NumberTheory/Fermat4.lean to Mathlib/NumberTheory/FLT/Four.lean

added theorem fermatLastTheoremFour

deleted theorem not_fermat_4