Open Research Index

Local class field theory in Lean 4.35.0-rc2

Naganori Yamaguchi

Palomar Registrypalomar/PALOMAR-2026-09-28-000002Sep 28, 2026math.NTscore 0

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.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-28-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-28-000002/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-28-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'