Engel’s theorem in Mathlib. (English) Zbl 07702724
Summary: We discuss the theory of Lie algebras in Lean’s Mathlib library. Using nilpotency as the theme, we outline a computer formalisation of Engel’s theorem and an application to root space theory. We emphasise that all arguments work with coefficients in any commutative ring.
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 17B30 | Solvable, nilpotent (super)algebras |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 68V20 | Formalization of mathematics in connection with theorem provers |
References:
| [1] | Bourbaki, N.: Lie Groups and Lie Algebras. Chapters 1-3. Elements of Mathematics (Berlin), p. 450. Springer, New York (1998). Translated from the French, Reprint of the 1989 English translation · Zbl 0902.13001 |
| [2] | Carneiro, M.: The type theory of lean. Master thesis (2019) |
| [3] | Dupuis, F., Lewis, R.Y., Macbeth, H.: Formalized functional analysis with semilinear maps. In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, OR, Israel (2022). arXiv:2202.05360 |
| [4] | Fulton, W., Harris, J.: Representation Theory. Graduate Texts in Mathematics, vol. 129, p. 551. Springer, New York (1991). doi:10.1007/978-1-4612-0979-9. A first course, Readings in Mathematics · Zbl 0744.22001 |
| [5] | Jacobson, N., Une généralisation du théorème d’Engel, C. R. Acad. Sci. Paris, 234, 579-581 (1952) · Zbl 0046.03401 |
| [6] | Nash, O.: Formalising Lie Algebras. Association for Computing Machinery, New York, NY, USA (2022). doi:10.1145/3497775.3503672 |
| [7] | Serre, J.-P.: Complex Semisimple Lie Algebras, p. 74. Springer, New York (1987). doi:10.1007/978-1-4757-3910-7 . Translated from the French by G. A. Jones · Zbl 0628.17003 |
| [8] | The mathlib community: The Lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pp. 367-381 (2020). doi:10.1145/3372885.3373824 |
| [9] | Zel’manov, EI, Solution of the restricted Burnside problem for groups of odd exponent, Izv. Akad. Nauk SSSR Ser. Mat., 54, 1, 42-59221 (1990) · Zbl 0704.20030 |
| [10] | Zorn, M., On a theorem of Engel, Bull. Am. Math. Soc., 43, 6, 401-404 (1937) · JFM 63.0345.03 · doi:10.1090/S0002-9904-1937-06565-7 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
