Gauss sums for Dirichlet characters #
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_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)
:
If χ is a primitive character, then the function a ↦ gaussSum χ (e.mulShift a), for any
fixed additive character e, is a constant multiple of χ⁻¹.