gaussSum — Mathlib

English

Definition of the Gauss sum associated to a multiplicative character χ and an additive character ψ: gaussSum(χ, ψ) = ∑_{a∈R} χ(a) ψ(a).

Русский

Определение гауссовой суммы, ассоциированной с мультипликативным символом χ и аддитивным ψ: gaussSum(χ, ψ) = ∑_{a∈R} χ(a) ψ(a).

LaTeX

$$$\mathrm{gaussSum}(\chi, \psi) = \sum_{a\in R} \chi(a) \psi(a)$$$

Lean4

/-- Definition of the Gauss sum associated to a multiplicative and an additive character. -/
def gaussSum (χ : MulChar R R') (ψ : AddChar R R') : R' :=
  ∑ a, χ a * ψ a

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