Yamaguchi Lean 4 Library

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.

Repository: https://github.com/n-yamaguchi-0729/ClassFieldTheory

A Lean 4 library for profinite and pro-C groups, including inverse systems, free pro-C groups, finite generation, completed group algebras, Fox differentials, Reidemeister–Schreier theory, and the Crowell exact sequence.

Repository: https://github.com/n-yamaguchi-0729/ProCGroups