Commit 2024-05-01 18:08 17f6b37d

feat(NumberTheory/DirichletCharacter): vanishing of Gauss sums when add char is imprimitive (#12324) The aim of this PR is to show that gaussSum χ e, for χ a Dirichlet character mod N and e an additive character mod N, is zero if χ is primitive but e is not. This will be used to prove the functional equation for Dirichlet L-series in a later PR. Along the way we add various general-purpose lemmas about divisibility in ZMod N and other finite rings, and about conductors and primitivity of Dirichlet and additive characters.