Commit 2024-02-19 19:19 4ae8a4dd

View on Github →

feat: basic theory of chains of roots / weights of Lie algebras / modules (#10548)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Lie/Killing.lean

Modified Mathlib/Algebra/Lie/OfAssociative.lean

added theorem Module.End.lie_apply

Modified Mathlib/Algebra/Lie/Submodule.lean

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

added theorem LieModule.lie_mem_weightSpaceChain_of_weightSpace_eq_bot_left

added theorem LieModule.lie_mem_weightSpaceChain_of_weightSpace_eq_bot_right

added theorem LieModule.trace_toEndomorphism_weightSpaceChain_eq_zero

added def LieModule.weightSpaceChain

added theorem LieModule.weightSpaceChain_def'

added theorem LieModule.weightSpaceChain_def

added theorem LieModule.weightSpaceChain_neg

added theorem LieModule.weightSpace_le_weightSpaceChain

Modified Mathlib/Order/CompleteLattice.lean

added theorem Equiv.biInf_comp

added theorem Equiv.biSup_comp