FC10 — Serre, Local Fields

This book contains 183 definitions, 41 theorems, 159 propositions, 49 lemmas, 115 corollaries, 34 examples, 46 conventions and 9 other statements.

636 of its 636 statements have been checked against Lean; 103 of those are formalized somewhere.

Chapter Definitions Theorems, propositions Lemmas, corollaries Everything else Formalized Not formalized
FC10 — Jean-Pierre Serre, Local Fields (1979) 30 23 13 17 36 47
FC10 — Jean-Pierre Serre, Local Fields (1979) 14 18 12 7 9 42
FC10 — Jean-Pierre Serre, Local Fields (1979) 9 17 13 3 5 37
FC10 — Jean-Pierre Serre, Local Fields (1979) 12 19 18 6 0 55
FC10 — Jean-Pierre Serre, Local Fields (1979) 4 13 26 3 0 46
FC10 — Jean-Pierre Serre, Local Fields (1979) 18 7 6 4 5 30
FC10 — Jean-Pierre Serre, Local Fields (1979) 30 10 2 3 22 23
FC10 — Jean-Pierre Serre, Local Fields (1979) 12 9 6 2 12 17
FC10 — Jean-Pierre Serre, Local Fields (1979) 3 15 14 1 4 29
FC10 — Jean-Pierre Serre, Local Fields (1979) 16 11 7 12 4 42
FC10 — Jean-Pierre Serre, Local Fields (1979) 14 8 5 12 4 35
FC10 — Jean-Pierre Serre, Local Fields (1979) — 6 5 2 0 13
FC10 — Jean-Pierre Serre, Local Fields (1979) 8 17 12 6 0 43
FC10 — Jean-Pierre Serre, Local Fields (1979) 12 19 13 7 2 49
FC10 — Jean-Pierre Serre, Local Fields (1979) 1 8 12 4 0 25

What the book contains

Kind of statement Count
Definitions 183
Theorems 41
Propositions 159
Lemmas 49
Corollaries 115
Examples 34
Conventions 46
Other statements 9
Total 636

Where its statements stand in Lean

Status Statements Share What it means
not formalized 533 84% A documented search found no Lean statement of it anywhere.
in Mathlib 85 13% Mathlib states and proves it.
in another Lean project 16 3% Some other Lean development has it; using it means porting that code.
in lean-categories 2 0% This repository states and proves it.
checked in total 636

How this book was read

Corpus source: FC10 in Foundational source corpus v1 (frozen).

Frozen source: Serre - 1979 - Local Fields.md.

Scope: complete book, Chapters I–XV and the global reciprocity appendix; exercises excluded item-by-item. Stable IDs are chapter-local and source-ordered after repair of OCR page-column interleavings; dependencies point only to strictly earlier FC10 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: 636 (376 formal/named main-text units; 22 explicitly labeled example units; 12 reusable member examples split from collection headings; 226 unnumbered definition/construction/convention units).