FC09 — Neukirch, Algebraic Number Theory
This book contains 296 definitions, 73 theorems, 245 propositions, 33 lemmas, 56 corollaries, 21 examples, 62 conventions and 17 other statements.
803 of its 803 statements have been checked against Lean; 168 of those are formalized somewhere.
| Chapter | Definitions | Theorems, propositions | Lemmas, corollaries | Everything else | Formalized | Not formalized |
|---|---|---|---|---|---|---|
| FC09 — Jürgen Neukirch, Algebraic Number Theory (1999) | 56 | 54 | 14 | 11 | 65 | 70 |
| FC09 — Jürgen Neukirch, Algebraic Number Theory (1999) | 54 | 58 | 10 | 13 | 32 | 103 |
| FC09 — Jürgen Neukirch, Algebraic Number Theory (1999) | 55 | 46 | 12 | 16 | 11 | 118 |
| FC09 — Jürgen Neukirch, Algebraic Number Theory (1999) | 29 | 32 | 3 | 19 | 23 | 60 |
| FC09 — Jürgen Neukirch, Algebraic Number Theory (1999) | 17 | 25 | 8 | 6 | 5 | 51 |
| FC09 — Jürgen Neukirch, Algebraic Number Theory (1999) | 30 | 41 | 12 | 7 | 4 | 86 |
| FC09 — Jürgen Neukirch, Algebraic Number Theory (1999) | 55 | 62 | 30 | 28 | 28 | 147 |
What the book contains
| Kind of statement | Count |
|---|---|
| Definitions | 296 |
| Theorems | 73 |
| Propositions | 245 |
| Lemmas | 33 |
| Corollaries | 56 |
| Examples | 21 |
| Conventions | 62 |
| Other statements | 17 |
| Total | 803 |
Where its statements stand in Lean
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 635 | 79% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 152 | 19% | Mathlib states and proves it. |
| in another Lean project | 12 | 1% | Some other Lean development has it; using it means porting that code. |
| in lean-categories | 4 | 0% | This repository states and proves it. |
| checked in total | 803 |
How this book was read
Corpus source: FC09 in Foundational source corpus v1 (frozen).
Frozen source: local-write-api-1783468319638-8698XMKC_extracted.md.
Scope: complete book, Chapters I–VII; end-of-section Exercises and Problems excluded item-by-item. Stable IDs are chapter-local and source-ordered; dependencies point only to strictly earlier FC09 units.
Inventory policy: definitions, constructions, conventions/notation, labeled theorems/propositions/corollaries/lemmas/axioms, named theorem statements, and reusable examples/comparisons. Exposition/history, local proof variables, and later recaps are excluded as separate units.
Candidate unit count: 803 (502 numbered main-text units; 21 explicit unnumbered examples/comparisons; 280 run-in definition/construction/convention units).