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
License
Topics
Session Gauss_Sums
- Gauss_Sums_Auxiliary
- Periodic_Arithmetic
- Complex_Roots_Of_Unity
- Finite_Fourier_Series
- Ramanujan_Sums
- Gauss_Sums
- Polya_Vinogradov