Additive character

Summary

An additive character of a ring or field $R$ is a character of the additive group $(R, +)$. It is a map $\psi$ to the nonzero complex numbers with $\psi(x + y) = \psi(x)\psi(y)$. The name contrasts it with a multiplicative character, which is a character of the group of units $R^\times$. Additive characters of finite fields are the building blocks of exponential sums, Gauss sums and the discrete Fourier transform on $\F_q$. In Mathlib, an additive character of an additive monoid $A$ with values in a monoid $M$ is a map $\psi \colon A \to M$ with $\psi(0) = 1$ and $\psi(a + b) = \psi(a)\psi(b)$.