Commit 2026-07-21 13:55 6e593caa

View on Github →

chore: make Cartan subalgebra a parameter of LieAlgebra.Basis rather than field (#41972) This allows greater definitional control over the Cartan subalgebra which turns out to be very useful in later work. The price is that LieAlgebra.Basis.isCartanSubalgebra and LieAlgebra.Basis.isLieAbelian_cartan must both be demoted from instance to lemma but overall the extra definitional control is a big win.

Estimated changes

Modified Mathlib/Algebra/Lie/Basis.lean

modified def LieAlgebra.Basis.base

modified def LieAlgebra.Basis.baseSupp'

modified def LieAlgebra.Basis.baseSupp

modified theorem LieAlgebra.Basis.baseSupp_apply_smul_e

modified theorem LieAlgebra.Basis.baseSupp_apply_smul_f

modified def LieAlgebra.Basis.borelLower

modified def LieAlgebra.Basis.borelUpper

modified theorem LieAlgebra.Basis.coe_cartan_eq_span

modified def LieAlgebra.Basis.h'

added theorem LieAlgebra.Basis.isCartanSubalgebra

added theorem LieAlgebra.Basis.isLieAbelian_cartan

modified theorem LieAlgebra.Basis.root_mem_or_mem_neg

modified def LieAlgebra.Basis.symm

modified structure LieAlgebra.Basis

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basis.lean