English
If χ is primitive, then gaussSum χ (e.mulShift a) equals χ⁻¹ a times gaussSum χ e; in the non-unit case, it is zero if a is not a unit or the shifted Gauss sum vanishes otherwise.
Русский
Если χ примитивен, то gaussSum χ (e.mulShift a) равно χ⁻¹ a умноженному на gaussSum χ e; если a не единица, то гауссова сумма равна нулю, иначе сохраняется.\n
LaTeX
$$$\\text{gaussSum\\_mulShift\\_of\\_isPrimitive}: gaussSum χ (e.mulShift a) = χ^{-1} a \\cdot gaussSum χ e.$ (когда a является единицей; иначе $gaussSum χ (e.mulShift a)=0$).$$
Lean4
/-- If `χ` is a primitive character, then the function `a ↦ gaussSum χ (e.mulShift a)`, for any
fixed additive character `e`, is a constant multiple of `χ⁻¹`. -/
theorem gaussSum_mulShift_of_isPrimitive [IsDomain R] {χ : DirichletCharacter R N} (hχ : IsPrimitive χ) (a : ZMod N) :
gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e :=
by
by_cases ha : IsUnit a
· conv_rhs => rw [← gaussSum_mulShift χ e ha.unit]
rw [IsUnit.unit_spec, MulChar.inv_apply_eq_inv, Ring.inverse_mul_cancel_left _ _ (ha.map χ)]
· rw [MulChar.map_nonunit _ ha, zero_mul]
exact gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive _ hχ (not_isPrimitive_mulShift e ha)
