Documentation

Mathlib.NumberTheory.DirichletCharacter.GaussSum

Gauss sums for Dirichlet characters #

source
๐Ÿ“ coverage
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
source
๐Ÿ“ coverage
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.)

source
๐Ÿ“ coverage
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.

source
๐Ÿ“ coverage
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 ฯ‡โปยน.