gaussSum_mul_gaussSum_eq_card in this pinned Mathlib is restricted to a finite-field source, so it cannot be specialized to ZMod N for a general conductor. The following is the exact ZMod N analogue needed here, obtained from ZMod.dft_dft; the proof of Fourier inversion itself uses ZMod.isPrimitive_stdAddChar. Thus this pays the same Gauss-sum cardinality identity without adding a primality hypothesis on N.

theorem DirichletCharacter.IsPrimitive.norm_rootNumber {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : χ.IsPrimitive) : ‖χ.rootNumber‖ = 1

The functional-equation root number of a primitive Dirichlet character has norm one.