Engel's theorem in Mathlib

DOI10.1007/S10817-023-09668-0MaRDI QIDQ6103593zbMATH OpenOpenAlexWikidataFDO

Authors Oliver Nash

Publication date 27 June 2023

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2304.10424

zbMATH Keywords

Engel's theoremformal mathLeanLie algebranilpotencyproof assistantroot space

Mathematics Subject Classification ID

Solvable, nilpotent (super)algebras (17B30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

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.

Cited in

(2)

• Formalization of the existence of Frobenius elements
• Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean

This page was built for publication: Engel's theorem in Mathlib

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6103593)