Commit 2026-06-25 16:37 609b527e

View on Github →

feat: add isCoprime_of_not_zeta_sub_one_dvd and related lemmas (#40906) From flt-regular.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean

added theorem IsPrimitiveRoot.toInteger_coe

Modified Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean

added theorem IsCyclotomicExtension.Rat.associated_sub_one_of_isPrimitiveRoot

added theorem IsCyclotomicExtension.Rat.associated_zeta_sub_one_pow_prime

added theorem IsCyclotomicExtension.Rat.isCoprime_of_not_zeta_sub_one_dvd

added theorem IsCyclotomicExtension.Rat.two_not_mem_span_zeta_sub_one'

Modified Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean

deleted theorem IsPrimitiveRoot.ntRootsFinset_pairwise_associated_sub_one_sub_of_prime

added theorem IsPrimitiveRoot.nthRootsFinset_pairwise_associated_sub_one_sub_of_prime