Commit 2023-11-28 14:12 4bfed3e4

feat: weights of Lie modules are linear functions (#8677) Since we have already proved Cartan subalgebras of Lie algebras with non-singular Killing forms are Abelian, the changes here mean that the following now works without any assumptions on characteristic:

example {K L : Type*} [Field K] [LieRing L] [LieAlgebra K L]
    [FiniteDimensional K L] [LieAlgebra.IsKilling K L]
    (H : LieSubalgebra K L) [H.IsCartanSubalgebra] :
    LieModule.LinearWeights K H L := inferInstance