Formalising the local compactness of the adele ring

Salvatore Mercuri

The adele ring of a number field is a central object in modern number theory. Its status as a locally compact topological ring is one of the key reasons why. We describe a formal p…