English
If the characteristic conditions hold and ψ is primitive, then gaussSum(χ, ψ)^{orderOf χ} equals χ(−1) · |F| · ∏_{i=1}^{orderOf χ − 1} J(χ, χ^i).
Русский
При соблюдении условий характеристики и примитивности ψ, g(χ, ψ)^{ord χ} = χ(−1) · |F| · ∏_{i=1}^{ord χ − 1} J(χ, χ^i).
LaTeX
$$$$ gaussSum(χ, ψ)^{\operatorname{orderOf}(χ)} = χ(-1) \cdot |F| \cdot \prod_{i=1}^{\operatorname{orderOf}(χ)-1} J(χ, χ^i). $$$$
Lean4
/-- If `χ` is a multiplicative character of order `n ≥ 2` on a finite field `F`,
then `g(χ)^n = χ(-1) * #F * J(χ,χ) * J(χ,χ²) * ... * J(χ,χⁿ⁻²)`. -/
theorem gaussSum_pow_eq_prod_jacobiSum {χ : MulChar F R} {ψ : AddChar F R} (hχ : 2 ≤ orderOf χ) (hψ : ψ.IsPrimitive) :
gaussSum χ ψ ^ orderOf χ = χ (-1) * Fintype.card F * ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i) :=
by
have := gaussSum_pow_eq_prod_jacobiSum_aux χ ψ (n := orderOf χ - 1) (by cutsat) (by cutsat)
apply_fun (gaussSum χ ψ * ·) at this
rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos (by cutsat)] at this
have hχ₁ : χ ≠ 1 := fun h ↦ ((orderOf_one (G := MulChar F R) ▸ h ▸ hχ).trans_lt Nat.one_lt_two).false
rw [this, ← mul_assoc, gaussSum_mul_gaussSum_pow_orderOf_sub_one hχ₁ hψ]
