Commit 2025-10-15 16:18 cb5b0e58

View on Github →

feat: add Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits (#30085) We add basic results about cyclotomic units. From flt-regular.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean

added theorem IsPrimitiveRoot.associated_pow_add_sub_sub_one

added theorem IsPrimitiveRoot.associated_pow_sub_one_pow_of_coprime

added theorem IsPrimitiveRoot.associated_sub_one_pow_sub_one_of_coprime

added theorem IsPrimitiveRoot.geom_sum_isUnit'

added theorem IsPrimitiveRoot.geom_sum_isUnit

added theorem IsPrimitiveRoot.ntRootsFinset_pairwise_associated_sub_one_sub_of_prime

added theorem IsPrimitiveRoot.pow_sub_one_eq_geom_sum_mul_geom_sum_inv_mul_pow_sub_one

added theorem IsPrimitiveRoot.pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum