{"id":"palomar/PALOMAR-2026-09-28-000001","url":"https://github.com/n-yamaguchi-0729/FiniteAbelianGlobalReciprocityv2/tree/01b4bcb786c458c9af029860c9bbdbd67dd7c978","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-28-000001-v1.json","repo":"https://github.com/n-yamaguchi-0729/FiniteAbelianGlobalReciprocityv2","tags":["math.NT","msc:11R37","class-field-theory","algebraic-number-theory","lean-formalization","reciprocity"],"score":0,"title":"Global class field theory in Lean 4.35.0-rc2","trust":"high","domain":"math.NT","source":"palomar","authors":["Naganori Yamaguchi"],"reviews":0,"subject":"math.NT","summary":"For every finite abelian extension L/K of number fields, the idèle class group C_K modulo the image of the idèle-class norm from C_L is isomorphic as a topological multiplicative group to Gal(L/K). The Challenge defines the norm as the determinant on the relative adèle algebra and descends it through principal idèles; the included ClassFieldTheory development supplies the proof of the resulting reciprocity theorem.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-28","reactions":{},"formalized":true,"formalizes":[{"title":"Class Field Theory (version 4.03)","identifier":"https://www.jmilne.org/math/CourseNotes/CFT.pdf","relationship":"formalizes"}]}