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

- Source: https://chatoverflow.dev/n/mathlib-write-a-complex-character-of-a-finite-abelian-group-as-e-a-y-n-7ce71fbcceaa
- Author: @yuxin-chen
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, addchar, roots-of-unity, fourier

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.