Commit 2026-03-25 09:29 145f3f49

View on Github →

feat: define bases of semisimple Lie algebras and add API (#36298)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Basis.lean

added theorem LieAlgebra.Basis.A_diag_eq_two

added def LieAlgebra.Basis.base

added def LieAlgebra.Basis.baseSupp'

added def LieAlgebra.Basis.baseSupp

added theorem LieAlgebra.Basis.baseSupp_apply_h'

added theorem LieAlgebra.Basis.baseSupp_apply_smul_e

added theorem LieAlgebra.Basis.baseSupp_apply_smul_f

added def LieAlgebra.Basis.baseSupportEquiv

added def LieAlgebra.Basis.borelLower

added theorem LieAlgebra.Basis.borelLower_eq

added theorem LieAlgebra.Basis.borelLower_le_biSup

added def LieAlgebra.Basis.borelUpper

added theorem LieAlgebra.Basis.borelUpper_eq

added theorem LieAlgebra.Basis.borelUpper_le_biSup

added theorem LieAlgebra.Basis.cartanMatrix_base_eq

added theorem LieAlgebra.Basis.cartan_eq

added theorem LieAlgebra.Basis.coe_baseSupportEquiv_apply

added theorem LieAlgebra.Basis.coe_cartan_eq_span

added theorem LieAlgebra.Basis.coe_linearMap_baseSupp'

added theorem LieAlgebra.Basis.coroot_eq_h'

added def LieAlgebra.Basis.h'

added theorem LieAlgebra.Basis.iSupIndep_rootSpace

added theorem LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top

added theorem LieAlgebra.Basis.linearIndepOn_root_baseSupp

added theorem LieAlgebra.Basis.linearIndependent_baseSupp

added theorem LieAlgebra.Basis.root_mem_or_mem_neg

added def LieAlgebra.Basis.symm

added theorem LieAlgebra.Basis.symm_baseSupp

added theorem LieAlgebra.Basis.symm_h'

added theorem LieAlgebra.Basis.symm_symm

added structure LieAlgebra.Basis

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

added theorem Module.Basis.span_neg