Commit 2024-04-16 22:37 fcf5d484

View on Github →

Feat: add fermatLastTheoremThree_of_three_dvd_only_c (#11767) We add fermatLastTheoremThree_of_three_dvd_only_c: To prove FermatLastTheoremFor 3, we may assume that ¬ 3 ∣ a, ¬ 3 ∣ b, a and b are coprime and 3 ∣ c. From the flt3 project in LFTCM2024.

Estimated changes

Modified Mathlib/Data/Int/GCD.lean

modified theorem Int.pow_dvd_pow_iff

Modified Mathlib/Data/Nat/GCD/Basic.lean

modified theorem Nat.pow_dvd_pow_iff

Modified Mathlib/Data/Real/Irrational.lean

Modified Mathlib/NumberTheory/FLT/Basic.lean

added theorem dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT

added theorem isCoprime_of_gcd_eq_one_of_FLT

Modified Mathlib/NumberTheory/FLT/Four.lean

Modified Mathlib/NumberTheory/FLT/Three.lean

modified theorem fermatLastTheoremThree_case_1

added theorem fermatLastTheoremThree_of_three_dvd_only_c

Modified Mathlib/NumberTheory/Pell.lean

Modified Mathlib/NumberTheory/PythagoreanTriples.lean

Modified Mathlib/RingTheory/IntegrallyClosed.lean

added theorem IsIntegrallyClosed.pow_dvd_pow_iff