Commit 2024-05-22 12:09 d082b61f

View on Github →

feat: Lie algebra root spaces are 1-dimensional (#12937) over a field of characteristic zero, when the Killing form is non-singular

Estimated changes

Modified Mathlib/Algebra/Lie/Weights/Basic.lean

added theorem LieModule.Weight.exists_ne_zero

added theorem LieModule.Weight.ext

Modified Mathlib/Algebra/Lie/Weights/Cartan.lean

Modified Mathlib/Algebra/Lie/Weights/Killing.lean

added theorem IsSl2Triple.h_eq_coroot

added theorem LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton'

added theorem LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero

added theorem LieAlgebra.IsKilling.finrank_rootSpace_eq_one

modified theorem LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra

added theorem LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg

added theorem LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux

added theorem LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace

Modified Mathlib/Algebra/Lie/Weights/Linear.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean

added theorem Module.End.IsSemisimple.maxGenEigenspace_eq_eigenspace

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

added theorem LinearMap.ker_ne_bot_of_finrank_lt