Commit 2024-02-22 16:20 1e5697b8

View on Github →

feat: add lemma LieAlgebra.IsKilling.eq_zero_of_apply_eq_zero_of_mem_rootSpaceProductNegSelf (#10803)

Estimated changes

Modified Mathlib/Algebra/Lie/Killing.lean

added theorem LieAlgebra.IsKilling.eq_zero_of_apply_eq_zero_of_mem_rootSpaceProductNegSelf

added theorem LieAlgebra.IsKilling.iInf_ker_weight_eq_bot

added theorem LieAlgebra.IsKilling.ker_weight_inf_rootSpaceProductNegSelf_eq_bot

added theorem LieAlgebra.IsKilling.rootSpaceProductNegSelf_zero_eq_bot

modified theorem LieAlgebra.IsKilling.span_weight_eq_top

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

Modified Mathlib/LinearAlgebra/Dual.lean

added theorem Dual.apply_one_mul_eq

added theorem LinearMap.dualMap_eq_lcomp

added theorem LinearMap.range_dualMap_dual_eq_span_singleton