Commit 2024-06-25 09:57 5bdfd1ad

View on Github →

feat(Mathlib.NumberTheory.Cyclotomic.Three): add various results (#13798) We add various results about the third cyclotomic field needed to prove flt3. From the flt3 project at LFTCM2024.

Estimated changes

Modified Mathlib/Algebra/CharP/CharAndCard.lean

added theorem charP_of_card_eq_prime

Modified Mathlib/Data/ZMod/Basic.lean

added theorem ZMod.ringEquivOfPrime_eq_ringEquiv

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

added theorem IsPrimitiveRoot.card_quotient_toInteger_sub_one

added theorem IsPrimitiveRoot.coe_toInteger

added theorem IsPrimitiveRoot.finite_quotient_toInteger_sub_one

Modified Mathlib/NumberTheory/Cyclotomic/Three.lean

added theorem IsCyclotomicExtension.Rat.Three.coe_eta

added theorem IsCyclotomicExtension.Rat.Three.cube_sub_one_eq_mul

added theorem IsCyclotomicExtension.Rat.Three.eta_sq_add_eta_add_one

added theorem IsCyclotomicExtension.Rat.Three.lambda_dvd_mul_sub_one_mul_sub_eta_add_one

added theorem IsCyclotomicExtension.Rat.Three.lambda_dvd_or_dvd_sub_one_or_dvd_add_one

added theorem IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_add_one_of_dvd_add_one

added theorem IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one

added theorem IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd

Modified Mathlib/NumberTheory/FLT/Three.lean

Modified Mathlib/RingTheory/Fintype.lean

added theorem Finset.univ_of_card_le_three

added theorem Finset.univ_of_card_le_two