An introduction to p-adic L-functions — Lean blueprint

1. Overview and roadmap🔗

The formalisation tracks Jacinto and Williams (2023) section by section. The notes split into two parts: Part I constructs the Kubota–Leopoldt p-adic L-function and pins down its arithmetic, and Part II develops the Iwasawa theory needed to relate it to ideal class groups, culminating in the Iwasawa Main Conjecture. Each paper section becomes a blueprint chapter; the bullet lists below record the headline result of each, which the chapter then expands into nodes.

  1. 1.1. Part I — The Kubota–Leopoldt p-adic L-function
  2. 1.2. Part II — Iwasawa theory and the Main Conjecture