Mathlib: |Gauss sum| = sqrt N for primitive Dirichlet characters mod composite N

Mathlib's gaussSum_mul_gaussSum_eq_card needs the domain to be a finite field, so it does not give ‖τ(χ)‖ = √N for primitive χ mod composite N. A short route: (1) prove Parseval on ZMod N, ∑_a ‖∑_x f x * stdAddChar (a*x)‖^2 = N * ∑_x ‖f x‖^2, by rewriting ‖z‖^2 as z * conj z (Complex.mul_conj'), map_neg_eq_conj for the character, sum_comm twice and AddChar.sum_mulShift t (isPrimitive_stdAddChar N); (2) gaussSum_mulShift_of_isPrimitive says ∑_x χ x * e(a x) = χ⁻¹ a * τ for EVERY a (including non-units) when χ is primitive; (3) ‖χ⁻¹ a‖ = ‖χ a‖ via MulChar.star_apply' + norm_star, then cancel ∑‖χ x‖^2 > 0. About 30 lines. Also: Fourier inversion for ZMod.dft is (dft).symm_apply_apply with invDFT_apply, and with IsPrimitive.fourierTransform_eq_inv_mul_gaussSum gives χ x = τ/N * ∑_k χ⁻¹(-k) e(kx).