FC13 — Matsumura, Commutative Ring Theory
This book contains 198 definitions, 316 theorems, 3 propositions, 45 lemmas, 44 corollaries, 42 examples, 13 counterexamples, 38 constructions, 11 remarks, 4 conventions, 3 notations, 10 formulas, 6 criteria and 7 other statements.
672 of its 740 statements have been checked against Lean; 234 of those are formalized somewhere.
| Chapter | Definitions | Theorems, propositions | Lemmas, corollaries | Everything else | Formalized | Not formalized |
|---|---|---|---|---|---|---|
| Front matter — conventions and terminology | — | — | — | 5 | 5 | 0 |
| Chapter 1. Commutative rings and modules | 21 | 21 | 9 | 14 | 50 | 15 |
| Chapter 2. Prime ideals | 31 | 34 | 11 | 16 | 50 | 42 |
| Chapter 3. Properties of extension rings | 13 | 39 | 6 | 15 | 40 | 33 |
| Chapter 4. Valuation rings | 15 | 21 | 6 | 5 | 17 | 30 |
| Chapter 5. Dimension theory | 17 | 32 | 3 | 14 | 11 | 55 |
| Chapter 6. Regular sequences | 14 | 31 | 9 | 8 | 20 | 42 |
| Chapter 7. Regular rings | 14 | 27 | 8 | 6 | 19 | 36 |
| Chapter 8. Flatness revisited | 5 | 23 | 6 | 9 | 2 | 41 |
| Chapter 9. Derivations | 13 | 22 | 2 | 11 | 13 | 35 |
| Chapter 10. I-smoothness | 15 | 28 | 14 | 8 | 4 | 61 |
| Chapter 11. Applications of complete local rings | 11 | 23 | 14 | 3 | 3 | 48 |
| Appendix A. Tensor products, direct and inverse limits | 10 | 2 | — | 15 | not checked | |
| Appendix B. Some homological algebra | 15 | 11 | 1 | 1 | not checked | |
| Appendix C. The exterior algebra | 4 | 5 | — | 4 | not checked |
What the book contains
| Kind of statement | Count |
|---|---|
| Definitions | 198 |
| Theorems | 316 |
| Propositions | 3 |
| Lemmas | 45 |
| Corollaries | 44 |
| Examples | 42 |
| Counterexamples | 13 |
| Constructions | 38 |
| Remarks | 11 |
| Conventions | 4 |
| Notations | 3 |
| Formulas | 10 |
| Criteria | 6 |
| Other statements | 7 |
| Total | 740 |
Where its statements stand in Lean
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 438 | 65% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 197 | 29% | Mathlib states and proves it. |
| in another Lean project | 33 | 5% | Some other Lean development has it; using it means porting that code. |
| in lean-categories | 4 | 1% | This repository states and proves it. |
| checked in total | 672 |
How this book was read
Pinned source: Hideyuki Matsumura, Commutative Ring Theory, Cambridge Studies in Advanced Mathematics 8, translated by Miles Reid; local pinned PDF local-write-api-1781955283942-TSA7KUJB_matsumura.pdf.
Extraction: Matsumura - Commutative Ring Theory.md (329 PDF pages; source-faithful page markers).
Coverage rule: complete main text, including mathematical front-matter conventions and Appendices A–C; exercises, solutions/hints, bibliography, and index are excluded as unit sources. The index is used only as a completeness audit for definitions.
Coverage: 740 source units. Namespace counts: C00=5, C01=65, C02=92, C03=73, C04=47, C05=66, C06=62, C07=55, C08=43, C09=48, C10=65, C11=51, CA=27, CB=28, CC=13.