English
Let χ be a multiplicative character of order n and ψ a primitive additive character. Then gaussSum χ ψ ^ n equals gaussSum χ^n ψ times a product of jacobiSum(χ, χ^j) for j = 1,...,n−1.
Русский
Пусть χ — мультипликативный символ порядка n, ψ — примитивный аддитивный символ. Тогда gaussSum(χ, ψ)^n равен gaussSum(χ^n, ψ) умноженное на ∏_{j=1}^{n−1} J(χ, χ^j).
LaTeX
$$$$ gaussSum(χ, ψ)^n = gaussSum(χ^n, ψ) \cdot \prod_{j=1}^{n-1} J(χ, χ^j). $$$$
Lean4
theorem gaussSum_pow_eq_prod_jacobiSum_aux (χ : MulChar F R) (ψ : AddChar F R) {n : ℕ} (hn₁ : 0 < n)
(hn₂ : n < orderOf χ) : gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j) := by
induction n, hn₁ using Nat.le_induction with
| base => simp only [pow_one, le_refl, Ico_eq_empty_of_le, prod_empty, mul_one]
| succ n hn ih =>
specialize ih <| lt_trans (Nat.lt_succ_self n) hn₂
have gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ :=
by
have hχn : χ * (χ ^ n) ≠ 1 := pow_succ' χ n ▸ pow_ne_one_of_lt_orderOf n.add_one_ne_zero hn₂
rw [mul_comm, ← jacobiSum_mul_nontrivial hχn, mul_comm, ← pow_succ']
apply_fun (· * gaussSum χ ψ) at ih
rw [mul_right_comm, ← pow_succ, gauss_rw] at ih
rw [ih, Finset.prod_Ico_succ_top hn, mul_rotate, mul_assoc]
