Commit 2024-02-22 09:41 3718a428

View on Github →

feat: add lemma LieModule.exists_pos_smul_add_smul_rootSpaceProductNegSelf_eq_zero (#10748)

Estimated changes

Modified Mathlib/Algebra/Lie/Killing.lean

deleted theorem LieModule.trace_toEndomorphism_weightSpace

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

added theorem LieModule.trace_toEndomorphism_weightSpace

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

added theorem LieModule.eventually_weightSpace_smul_add_eq_bot

added theorem LieModule.exists_forall_mem_rootSpaceProductNegSelf_smul_add_eq_zero

added theorem LieModule.exists_weightSpace_smul_add_eq_bot

added theorem LieModule.exists₂_weightSpace_smul_add_eq_bot

modified theorem LieModule.trace_toEndomorphism_weightSpaceChain_eq_zero

Modified Mathlib/Order/Filter/Cofinite.lean

added theorem Nat.eventually_pos

Modified docs/references.bib