Commit 2024-05-28 10:02 40905830

View on Github →

feat(Algebra/Lie/Weights): n such that n • α + β is a weight is consecutive. (#13298)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Weights/RootSystem.lean

added theorem LieAlgebra.IsKilling.apply_coroot_eq_cast'

added theorem LieAlgebra.IsKilling.apply_coroot_eq_cast

added theorem LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff

added theorem LieAlgebra.IsKilling.chainBotCoeff_le_chainLength

added theorem LieAlgebra.IsKilling.chainBotCoeff_of_eq_zsmul_add

added def LieAlgebra.IsKilling.chainLength

added theorem LieAlgebra.IsKilling.chainLength_neg

added theorem LieAlgebra.IsKilling.chainLength_nsmul

added theorem LieAlgebra.IsKilling.chainLength_of_eq_zsmul_add

added theorem LieAlgebra.IsKilling.chainLength_of_isZero

added theorem LieAlgebra.IsKilling.chainLength_smul

added theorem LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff

added theorem LieAlgebra.IsKilling.chainTopCoeff_le_chainLength

added theorem LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add

added theorem LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top

added theorem LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_le

added theorem LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt

added theorem LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff

added theorem LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem