Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-07 12:02 41ec92ea

View on Github →

feat(algebra/lie/from_cartan_matrix): construction of a Lie algebra from a Cartan matrix (#8206)

Estimated changes

Modified docs/references.bib

Created src/algebra/lie/from_cartan_matrix.lean

added inductive cartan_matrix.generators

added def cartan_matrix.relations.EF

added def cartan_matrix.relations.HE

added def cartan_matrix.relations.HF

added def cartan_matrix.relations.HH

added def cartan_matrix.relations.ad_E

added def cartan_matrix.relations.ad_F

added def cartan_matrix.relations.to_ideal

added def cartan_matrix.relations.to_set

added def matrix.to_lie_algebra