Commit 2023-11-29 10:17 345c6ba7

feat: the roots of a Lie algebra with non-singular Killing form span the dual of the Cartan subalgebra (#8688) In combination with existing work the changes here mean that the following now works (and furthermore, makes no assumptions about characteristic):

example {K L : Type*} [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L]
    [FiniteDimensional K L] [LieAlgebra.IsKilling K L]
    (H : LieSubalgebra K L) [H.IsCartanSubalgebra] :
    Submodule.span K (range (LieModule.weight.toLinear K H L)) = ⊤ := by
  simp