Commit 2024-05-27 17:25 f1fd937b

View on Github →

feat(Algebra/Lie/Weights/Chain): More API for chains. (#13258)

Estimated changes

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

added def LieModule.chainBot

added def LieModule.chainBotCoeff

added theorem LieModule.chainBotCoeff_neg

added theorem LieModule.chainBotCoeff_zero

added theorem LieModule.chainBot_neg

added theorem LieModule.chainBot_zero

added def LieModule.chainTop

added def LieModule.chainTopCoeff

added theorem LieModule.chainTopCoeff_add_one

added theorem LieModule.chainTopCoeff_neg

added theorem LieModule.chainTopCoeff_zero

added theorem LieModule.chainTop_isNonZero'

added theorem LieModule.chainTop_isNonZero

added theorem LieModule.chainTop_neg

added theorem LieModule.chainTop_zero

added theorem LieModule.coe_chainBot

added theorem LieModule.coe_chainTop'

added theorem LieModule.coe_chainTop

added theorem LieModule.weightSpace_add_chainTop

added theorem LieModule.weightSpace_chainBotCoeff_sub_one_zsmul_sub

added theorem LieModule.weightSpace_chainTopCoeff_add_one_nsmul_add

added theorem LieModule.weightSpace_chainTopCoeff_add_one_zsmul_add

added theorem LieModule.weightSpace_neg_add_chainBot

added theorem LieModule.weightSpace_neg_zsmul_add_ne_bot

added theorem LieModule.weightSpace_nsmul_add_ne_bot_of_le

added theorem LieModule.weightSpace_zsmul_add_ne_bot