Commit 2024-07-11 10:12 1a3e2c42

View on Github →

feat(Mathlib.NumberTheory.FLT.Three): add various results (#14227) We add various results needed to prove flt3. From the flt3 project at LFTCM2024.

Estimated changes

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

Modified Mathlib/Algebra/Ring/Divisibility/Lemmas.lean

added theorem dvd_mul_sub_mul_mul_gcd_of_dvd

added theorem dvd_mul_sub_mul_mul_left_of_dvd

added theorem dvd_mul_sub_mul_mul_right_of_dvd

Modified Mathlib/NumberTheory/Cyclotomic/Three.lean

added theorem IsCyclotomicExtension.Rat.Three.eta_sq

Modified Mathlib/NumberTheory/FLT/Three.lean

added theorem FermatLastTheoremForThreeGen.Solution.a_add_eta_mul_b

added theorem FermatLastTheoremForThreeGen.Solution.associated_of_dvd_a_add_b_of_dvd_a_add_eta_mul_b

added theorem FermatLastTheoremForThreeGen.Solution.associated_of_dvd_a_add_b_of_dvd_a_add_eta_sq_mul_b

added theorem FermatLastTheoremForThreeGen.Solution.associated_of_dvd_a_add_eta_mul_b_of_dvd_a_add_eta_sq_mul_b

added theorem FermatLastTheoremForThreeGen.Solution.eta_add_one_mul_neg_eta_eq_one

added theorem FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_mul_b

added theorem FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_sq_mul_b

added theorem FermatLastTheoremForThreeGen.Solution.lambda_pow_dvd_a_add_b

added theorem FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_mul_b

added theorem FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_sq_mul_b

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

added theorem exists_associated_pow_of_associated_pow_mul