{"id":"palomar/PALOMAR-2026-09-28-000002","url":"https://github.com/n-yamaguchi-0729/FiniteAbelianLocalReciprocityv2/tree/3b402b69622b131ebdc7ffe746c8975c593dc330","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-28-000002-v1.json","repo":"https://github.com/n-yamaguchi-0729/FiniteAbelianLocalReciprocityv2","tags":["math.NT","msc:11S31","lean","number-theory","class-field-theory","local-fields"],"score":0,"title":"Local 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 a nonarchimedean local field, the multiplicative group K× modulo the field-norm subgroup N_{L/K}(L×) is isomorphic as a topological group to Gal(L/K). The registered declaration is the finite norm-quotient form of local reciprocity proved in the included ClassFieldTheory development. Stronger compatibility, normalization and existence results in that development are documented separately and are not part of the compared declaration.","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"}]}