Gauss sums for Dirichlet characters

theorem gaussSum_aux_of_mulShift {N : ℕ} [NeZero N] {R : Type u_1} [CommRing R] (e : AddChar (ZMod N) R) (χ : DirichletCharacter R N) {d : ℕ} (hd : d ∣ N) (he : e.mulShift ↑d = 1) {u : (ZMod N)ˣ} (hu : (ZMod.unitsMap hd) u = 1) : χ ↑u * gaussSum χ e = gaussSum χ e

theorem factorsThrough_of_gaussSum_ne_zero {N : ℕ} [NeZero N] {R : Type u_1} [CommRing R] (e : AddChar (ZMod N) R) [IsDomain R] {χ : DirichletCharacter R N} {d : ℕ} (hd : d ∣ N) (he : e.mulShift ↑d = 1) (h_ne : gaussSum χ e ≠ 0) : χ.FactorsThrough d

If gaussSum χ e ≠ 0, and d is such that e.mulShift d = 1, then χ must factor through d. (This will be used to show that Gauss sums vanish when χ is primitive and e is not.)

theorem gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive {N : ℕ} [NeZero N] {R : Type u_1} [CommRing R] (e : AddChar (ZMod N) R) [IsDomain R] {χ : DirichletCharacter R N} (hχ : χ.IsPrimitive) (he : ¬e.IsPrimitive) : gaussSum χ e = 0

If χ is primitive, but e is not, then gaussSum χ e = 0.

theorem gaussSum_mulShift_of_isPrimitive {N : ℕ} [NeZero N] {R : Type u_1} [CommRing R] (e : AddChar (ZMod N) R) [IsDomain R] {χ : DirichletCharacter R N} (hχ : χ.IsPrimitive) (a : ZMod N) : gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e

If χ is a primitive character, then the function a ↦ gaussSum χ (e.mulShift a), for any fixed additive character e, is a constant multiple of χ⁻¹.