FC04 — Atiyah & Macdonald, Introduction to Commutative Algebra
This book contains 126 definitions, 22 theorems, 97 propositions, 13 lemmas, 52 corollaries, 13 examples, 2 counterexamples, 44 constructions, 1 remark, 5 conventions, 4 notations and 54 other statements.
336 of its 433 statements have been checked against Lean; 246 of those are formalized somewhere.
| Chapter | Definitions | Theorems, propositions | Lemmas, corollaries | Everything else | Formalized | Not formalized |
|---|---|---|---|---|---|---|
| Chapter 1. Rings and Ideals (pp. 1–9) | 25 | 13 | 2 | 19 | 53 | 6 |
| Chapter 2. Modules (pp. 17–30) | 24 | 15 | 3 | 27 | not checked | |
| Chapter 3. Rings and Modules of Fractions (pp. 36–42) | 4 | 10 | 6 | 13 | 27 | 6 |
| Chapter 4. Primary Decomposition (pp. 50–54) | 9 | 8 | 3 | 9 | 19 | 10 |
| Chapter 5. Integral Dependence and Valuations (pp. 59–66) | 9 | 13 | 11 | 6 | 32 | 7 |
| Chapter 6. Chain Conditions (pp. 74–77) | 16 | 10 | 2 | 2 | 28 | 2 |
| Chapter 7. Noetherian Rings (pp. 80–83) | 1 | 9 | 8 | 1 | 19 | 0 |
| Chapter 8. Artin Rings (pp. 89–90) | 1 | 7 | 1 | 4 | 10 | 3 |
| Chapter 9. Discrete Valuation Rings and Dedekind Domains (pp. 93–98) | 8 | 7 | 2 | 12 | 1 | 0 |
| Chapter 10. Completions (pp. 100–112) | 15 | 14 | 13 | 18 | 39 | 21 |
| Chapter 11. Dimension Theory (pp. 116–124) | 14 | 13 | 14 | 12 | 18 | 35 |
What the book contains
| Kind of statement | Count |
|---|---|
| Definitions | 126 |
| Theorems | 22 |
| Propositions | 97 |
| Lemmas | 13 |
| Corollaries | 52 |
| Examples | 13 |
| Counterexamples | 2 |
| Constructions | 44 |
| Remarks | 1 |
| Conventions | 5 |
| Notations | 4 |
| Other statements | 54 |
| Total | 433 |
Where its statements stand in Lean
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 223 | 66% | Mathlib states and proves it. |
| not formalized | 90 | 27% | A documented search found no Lean statement of it anywhere. |
| in lean-categories | 17 | 5% | This repository states and proves it. |
| in another Lean project | 4 | 1% | Some other Lean development has it; using it means porting that code. |
| in a Lean package | 2 | 1% | A library available as a Lake dependency has it. |
| checked in total | 336 |
How this book was read
Corpus source: FC04 in Foundational source corpus v1 (frozen).
Pinned source: M. F. Atiyah and I. G. Macdonald, Introduction to Commutative Algebra, Addison–Wesley, 1969; complete book, exercises excluded.
Markdown extraction: local-write-api-1783448143508-XL7FDEDH_extracted.md.
This is the canonical Sweep-I source-unit catalogue for FC04. Stable source-local IDs are consumed unchanged by Sweeps II–IV.
Chapters 1–6: 259 units.
Chapters 7–11: 174 units.
Total: 433 stable source units.
Explicit main-text Lemma/Proposition/Theorem/Corollary introductions: 183.
Exercises are excluded, including embedded exercises in Chapters 1–3; all recorded dependencies are earlier FC04 unit IDs.