Engel's theorem in Mathlib

DOI10.1007/s10817-023-09668-0arXiv2304.10424OpenAlexW4382446539WikidataQ121873878 ScholiaQ121873878MaRDI QIDQ6103593

Oliver Nash

Publication date: 27 June 2023

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

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

zbMATH Keywords

Lie algebraroot spacenilpotencyproof assistantEngel's theoremLeanformal math

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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