Commit 2020-05-01 15:51 4daa7e8f

feat(algebra/lie_algebra): define simple Lie algebras and define classical Lie algebra, slₙ (#2567) The changes here introduce a few important properties of Lie algebras and also begin providing definitions of the classical Lie algebras. The key changes are the following definitions:

• lie_algebra.is_abelian
• lie_module.is_irreducible
• lie_algebra.is_simple
• lie_algebra.special_linear.sl Some simple related proofs are also included such as:
• commutative_ring_iff_abelian_lie_ring
• lie_algebra.special_linear.sl_non_abelian