All.lean

Global reciprocity

This public root exports global Artin maps, cyclotomic comparisons, local norm kernels, the principal-idèle product formula, the concrete cyclotomic idèle-class valuation, local--global compatibility, and the descended global norm-residue homomorphism with its actual norm-range kernel. It also exports the finite- and infinite-place Kummer-character comparison, the all-place Hilbert product formula, general power-residue reciprocity with explicit bad-place correction, and Gauss quadratic reciprocity over ℚ.