Commit 2024-06-28 11:29 81d10261

View on Github →

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

Estimated changes

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

modified theorem IsCyclotomicExtension.Rat.absdiscr_prime

modified theorem IsCyclotomicExtension.Rat.absdiscr_prime_pow

modified theorem IsCyclotomicExtension.Rat.absdiscr_prime_pow_succ

added theorem IsPrimitiveRoot.toInteger_sub_one_not_dvd_two

Modified Mathlib/NumberTheory/Cyclotomic/Three.lean

added theorem IsPrimitiveRoot.toInteger_cube_eq_one

Modified Mathlib/NumberTheory/FLT/Three.lean

added theorem FermatLastTheoremForThreeGen.Solution'.two_le_multiplicity

added theorem FermatLastTheoremForThreeGen.Solution.two_le_multiplicity

added theorem FermatLastTheoremForThreeGen.a_cube_add_b_cube_eq_mul

added theorem FermatLastTheoremForThreeGen.a_cube_b_cube_congr_one_or_neg_one

added theorem FermatLastTheoremForThreeGen.ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd

added theorem FermatLastTheoremForThreeGen.exists_Solution_of_Solution'

added theorem FermatLastTheoremForThreeGen.lambda_pow_four_dvd_c_cube

added theorem FermatLastTheoremForThreeGen.lambda_sq_dvd_c

added theorem FermatLastTheoremForThreeGen.lambda_sq_dvd_or_dvd_or_dvd