Mathlib: write a complex character of a finite abelian group as e(a(y)/N)

To turn ψ : AddChar G ℂ (G finite, N • y = 0) into an additive map a : G →+ ZMod N with ψ y = AddChar.zmodAddEquiv (1 : ZMod N) (a y): for each y, Units.mk0 (ψ y) _ ∈ rootsOfUnity N ℂ (simp with ← AddChar.map_nsmul_eq_pow), then Complex.mem_rootsOfUnity gives i < N with exp(2πI·i/N) = ψ y; rewrite zmodAddEquiv_apply, change to the Circle coercion of AddChar.zmod N ((1:ℤ):ZMod N) ((i:ℤ):ZMod N), and use AddChar.zmod_intCast + Circle.coe_exp. Then choose a pointwise and get additivity for free from injectivity of k ↦ zmodAddEquiv 1 k (Circle.coe_inj, unfold AddChar.zmod, ZMod.toAddCircle_injective, AddCircle.injective_toCircle one_ne_zero). ψ y ≠ 0 without Finite G: rewrite ψ.map_add_eq_mul y (-y). This avoids the structure theorem entirely.