English
For χ, ψ, χ(−1) · gaussSum χ ψ⁻¹ = gaussSum χ ψ (same as earlier).
Русский
Для χ, ψ, χ(−1) · gaussSum χ ψ⁻¹ = gaussSum χ ψ.
LaTeX
$$$\chi(-1) \cdot \mathrm{gaussSum}(\chi, ψ^{-1}) = \mathrm{gaussSum}(\chi, ψ)$$$
Lean4
/-- If the square of the Gauss sum of a quadratic character is `χ(-1) * #R`,
then we get, for all `n : ℕ`, the relation `(χ(-1) * #R) ^ (p^n/2) = χ(p^n)`,
where `p` is the (odd) characteristic of the target ring `R'`.
This version can be used when `R` is not a field, e.g., `ℤ/8ℤ`. -/
theorem card_pow_char_pow {χ : MulChar R R'} (hχ : IsQuadratic χ) (ψ : AddChar R R') (p n : ℕ) [fp : Fact p.Prime]
[hch : CharP R' p] (hp : IsUnit (p : R)) (hp' : p ≠ 2) (hg : gaussSum χ ψ ^ 2 = χ (-1) * Fintype.card R) :
(χ (-1) * Fintype.card R) ^ (p ^ n / 2) = χ ((p : R) ^ n) :=
by
have : gaussSum χ ψ ≠ 0 := by
intro hf
rw [hf, zero_pow two_ne_zero, eq_comm, mul_eq_zero] at hg
exact
not_isUnit_prime_of_dvd_card
((CharP.cast_eq_zero_iff R' p _).mp <| hg.resolve_left (isUnit_one.neg.map χ).ne_zero) hp
rw [← hg]
apply mul_right_cancel₀ this
rw [← hχ.gaussSum_frob_iter p n hp ψ, ← pow_mul, ← pow_succ,
Nat.two_mul_div_two_add_one_of_odd (fp.1.eq_two_or_odd'.resolve_left hp').pow]
