Engel’s Theorem in Mathlib
| Autor: | Oliver Nash |
|---|---|
| Rok vydání: | 2023 |
| Předmět: | |
| Zdroj: | Journal of Automated Reasoning. 67 |
| ISSN: | 1573-0670 0168-7433 |
| DOI: | 10.1007/s10817-023-09668-0 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink