Engel's theorem in Mathlib
Logic in Computer Science
2023-04-21 v1 Representation Theory
Abstract
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.
Keywords
Cite
@article{arxiv.2304.10424,
title = {Engel's theorem in Mathlib},
author = {Oliver Nash},
journal= {arXiv preprint arXiv:2304.10424},
year = {2023}
}