mathlib3

8230606c - feat(ring_theory/roots_of_unity): add geom_sum_eq_zero (#16755)

feat(ring_theory/roots_of_unity): add geom_sum_eq_zero (#16755) We add `geom_sum_eq_zero`: the geometric sum of a primitive root of unity is `0`. From flt-regular