gaussSum_ne_zero_of_nontrivial — Mathlib

English

If χ is nontrivial quadratic and ψ primitive, then gaussSum χ ψ squared equals χ(-1) times card R.

Русский

Если χ не тривиален и квадратичен и ψ примитивна, то gaussSum χ ψ в квадрате равно χ(-1) умножить на card R.

LaTeX

$$$\mathrm{gaussSum}(χ, ψ)^2 = χ(-1) \cdot |R|$$$

Lean4

/-- The Gauss sum of a nontrivial character on a finite field does not vanish. -/
theorem gaussSum_ne_zero_of_nontrivial (h : (Fintype.card R : R') ≠ 0) {χ : MulChar R R'} (hχ : χ ≠ 1)
    {ψ : AddChar R R'} (hψ : ψ.IsPrimitive) : gaussSum χ ψ ≠ 0 := fun H ↦
  h.symm <| zero_mul (gaussSum χ⁻¹ _) ▸ H ▸ gaussSum_mul_gaussSum_eq_card hχ hψ

Похожие утверждения