English
Same invariant property for Gauss sums under mulShift with hd|N and hu conditions; χ(u) gaussSum χ e = gaussSum χ e.
Русский
Та же инвариантность гауссовой суммы при mulShift: χ(u) gaussSum χ e = gaussSum χ e.
LaTeX
$$$\\text{gaussSum\\_aux\\_of\\_mulShift}(χ,e)\\;: \\; χ(u)\\, gaussSum(χ,e)=gaussSum(χ,e).$$$
Lean4
/-- 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 factorsThrough_of_gaussSum_ne_zero [IsDomain R] {χ : DirichletCharacter R N} {d : ℕ} (hd : d ∣ N)
(he : e.mulShift d = 1) (h_ne : gaussSum χ e ≠ 0) : χ.FactorsThrough d :=
by
rw [DirichletCharacter.factorsThrough_iff_ker_unitsMap hd]
intro u hu
rw [MonoidHom.mem_ker, ← Units.val_inj, MulChar.coe_toUnitHom]
simpa only [Units.val_one, ne_eq, h_ne, not_false_eq_true, mul_eq_right₀] using gaussSum_aux_of_mulShift e χ hd he hu
