李代数的形式化
Formalising Lie algebras
摘要：
李代数是代数的一个重要类别，出现在整个数学和物理。我们在Lean的Mathlib库中报告李代数的形式化。虽然基本知识的谎言理论将有利于读者，没有假设;其目的是，整体主题将访问，即使读者不熟悉谎言理论。特别注意的是支付给建设的经典和例外李代数。由于这些结构，有可能陈述特征为零的代数闭域上的有限维半单李代数的分类定理。除了关注Lie理论，我们还旨在突出Mathlib的统一性。为此，我们包括成就的例子，只有同时依靠图书馆的几个分支。
英文摘要：
Lie algebras are an important class of algebras which arise throughout mathematics and physics. We report on the formalisation of Lie algebras in Lean's Mathlib library. Although basic knowledge of Lie theory will benefit the reader, none is assumed; the intention is that the overall themes will be accessible even to readers unfamiliar with Lie theory. Particular attention is paid to the construction of the classical and exceptional Lie algebras. Thanks to these constructions, it is possible to state the classification theorem for finite-dimensional semisimple Lie algebras over an algebraically closed field of characteristic zero. In addition to the focus on Lie theory, we also aim to highlight the unity of Mathlib. To this end, we include examples of achievements made possible only by leaning on several branches of the library simultaneously.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
