Library
ClassFieldTheory
A Lean 4 formalization of local and global class field theory. It proves local reciprocity and the local existence theorem; global Artin reciprocity and the finite and infinite abelian class-field correspondences; conductor theory, norm limitation, and principalization in the Hilbert class field. It also proves Hasse–Arf, local and global Kronecker–Weber, the Hilbert-symbol product formula, power-residue reciprocity, and derives Gauss's quadratic reciprocity.
Formalized results
- Local reciprocity and the local existence theorem.
- Global Artin reciprocity and finite and infinite abelian class-field correspondences.
- Conductor theory, norm limitation, and principalization in the Hilbert class field.
- Hasse–Arf and the local and global Kronecker–Weber theorems.
- The Hilbert-symbol product formula, power-residue reciprocity, and Gauss's quadratic reciprocity.