jacobiSum_eq_gaussSum_mul_gaussSum_div_gaussSum

English

If card(F) ≠ 0 in the target, then J(χ, φ) = gaussSum(χ, ψ) gaussSum(φ, ψ) / gaussSum(χφ, ψ).

Русский

Если целевой характер не ноль, то J(χ, φ) = gaussSum(χ, ψ) gaussSum(φ, ψ) / gaussSum(χφ, ψ).

LaTeX

$$$$ J(χ, φ) = \frac{ gaussSum(χ, ψ) \cdot gaussSum(φ, ψ) }{ gaussSum(χ φ, ψ) }. $$$$

Lean4

/-- If `χ` and `φ` are multiplicative characters on a finite field `F` with values
in another field `F'` and such that `χφ` is nontrivial, then `J(χ,φ) = g(χ) * g(φ) / g(χφ)`. -/
theorem jacobiSum_eq_gaussSum_mul_gaussSum_div_gaussSum (h : (Fintype.card F : F') ≠ 0) {χ φ : MulChar F F'}
    (hχφ : χ * φ ≠ 1) {ψ : AddChar F F'} (hψ : ψ.IsPrimitive) :
    jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ / gaussSum (χ * φ) ψ :=
  by
  rw [eq_div_iff <| gaussSum_ne_zero_of_nontrivial h hχφ hψ, mul_comm]
  exact jacobiSum_mul_nontrivial hχφ ψ

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