[Merged by Bors] - feat: add Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

[riccardobrasca]

We add basic results about cyclotomic units.

From flt-regular.

---

[github-actions]

PR summary 34812cd2a7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits (new file)	1317

---

Declarations diff

+ associated_pow_add_sub_sub_one
+ associated_pow_sub_one_pow_of_coprime
+ associated_sub_one_pow_sub_one_of_coprime
+ geom_sum_isUnit
+ geom_sum_isUnit'
+ ntRootsFinset_pairwise_associated_sub_one_sub_of_prime
+ pow_sub_one_eq_geom_sum_mul_geom_sum_inv_mul_pow_sub_one
+ pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[faenuccio]

Thanks! Why not adding also

theorem geom_sum_isUnit' (hζ : IsPrimitiveRoot ζ n) (hj : j.Coprime n) (hj_Unit : IsUnit (j : A)) :
    IsUnit (∑ i ∈ range j, ζ ^ i) := by
  match n with
  | 0 => simp_all
  | 1 => simp_all
  | n +2 => exact geom_sum_isUnit hζ (by linarith) hj

[faenuccio]

Thanks, it all LGTM. Perhaps, before merging, can you add a line of todo (perhaps taken from your FLT project) so that other contributors might know what (not) to work on?

[faenuccio]

maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by faenuccio.

[riccardobrasca]

Thanks, it all LGTM. Perhaps, before merging, can you add a line of todo (perhaps taken from your FLT project) so that other contributors might know what (not) to work on?

This is essentially everything we have in flt-regular, so everything else has to be done

[Vierkantor]

Thanks! 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Post-Build Step
• Lint style