English
For χ, ψ and a unit a∈R^×, χ(a) · gaussSum(χ, mulShift(ψ, a)) = gaussSum(χ, ψ).
Русский
Для χ, ψ и единицы a∈R^×, χ(a) умножает гауссову сумму после подстановки mulShift(ψ, a), не изменяя сумму: χ(a)·gaussSum(χ, mulShift(ψ, a)) = gaussSum(χ, ψ).
LaTeX
$$$\chi(a) \cdot \mathrm{gaussSum}(\chi, \mathrm{mulShift}(\psi, a)) = \mathrm{gaussSum}(\chi, \psi)\quad (a \in R^{\times})$$$
Lean4
/-- Replacing `ψ` by `mulShift ψ a` and multiplying the Gauss sum by `χ a` does not change it. -/
theorem gaussSum_mulShift (χ : MulChar R R') (ψ : AddChar R R') (a : Rˣ) :
χ a * gaussSum χ (mulShift ψ a) = gaussSum χ ψ :=
by
simp only [gaussSum, mulShift_apply, Finset.mul_sum]
simp_rw [← mul_assoc, ← map_mul]
exact Fintype.sum_bijective _ a.mulLeft_bijective _ _ fun x ↦ rfl
