FC14 — Humphreys, Introduction to Lie Algebras and Representation Theory
This book contains 114 definitions, 54 theorems, 33 propositions, 67 lemmas, 36 corollaries, 12 examples, 48 constructions, 11 conventions, 2 notations, 4 formulas, 1 criterion and 2 other statements.
52 of its 384 statements have been checked against Lean; 31 of those are formalized somewhere.
| Chapter | Definitions | Theorems, propositions | Lemmas, corollaries | Everything else | Formalized | Not formalized |
|---|---|---|---|---|---|---|
| Chapter I. Basic Concepts | 24 | 6 | 4 | 18 | 31 | 21 |
| Chapter II. Semisimple Lie Algebras | 17 | 15 | 19 | 13 | not checked | |
| Chapter III. Root Systems | 22 | 10 | 22 | 12 | not checked | |
| Chapter IV. Isomorphism and Conjugacy Theorems | 7 | 8 | 14 | 6 | not checked | |
| Chapter V. Existence Theorem | 9 | 12 | 10 | 11 | not checked | |
| Chapter VI. Representation Theory | 21 | 23 | 23 | 12 | not checked | |
| Chapter VII. Chevalley Algebras and Groups | 14 | 13 | 11 | 8 | not checked |
What the book contains
| Kind of statement | Count |
|---|---|
| Definitions | 114 |
| Theorems | 54 |
| Propositions | 33 |
| Lemmas | 67 |
| Corollaries | 36 |
| Examples | 12 |
| Constructions | 48 |
| Conventions | 11 |
| Notations | 2 |
| Formulas | 4 |
| Criteria | 1 |
| Other statements | 2 |
| Total | 384 |
Where its statements stand in Lean
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 29 | 56% | Mathlib states and proves it. |
| not formalized | 21 | 40% | A documented search found no Lean statement of it anywhere. |
| in a Lean package | 2 | 4% | A library available as a Lake dependency has it. |
| checked in total | 52 |
How this book was read
Pinned source: J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Graduate Texts in Mathematics 9, third printing revised (1980).
Extraction: Humphreys - Introduction to Lie Algebras and Representation Theory.md (186 PDF pages, page-marked).
Coverage rule: complete mathematical content of the main text, including substantive section Notes and the mathematical Appendices; exercise blocks, bibliographic-only Notes, references, and indexes are excluded as unit sources. The terminology index is used only as a completeness audit.