### Abstract

This article provides a full formalisation of Chapter 8 of
Apostol's *Introduction
to Analytic Number Theory*. Subjects that are
covered are:

- periodic arithmetic functions and their finite Fourier series
- (generalised) Ramanujan sums
- Gauss sums and separable characters
- induced moduli and primitive characters
- the Pólya—Vinogradov inequality