Commit 2024-05-27 16:40 947168e0

View on Github →

feat(Algebra/Lie/*): Add Zero and Neg instances for weights. (#13261)

Estimated changes

Modified Mathlib/Algebra/Lie/CartanSubalgebra.lean

added theorem LieSubalgebra.ne_bot_of_isCartanSubalgebra

Modified Mathlib/Algebra/Lie/Submodule.lean

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

added theorem LieModule.Weight.coe_zero

added theorem LieModule.Weight.ext_iff

added theorem LieModule.Weight.isNonZero_iff_ne_zero

added theorem LieModule.Weight.isZero_iff_eq_zero

added theorem LieModule.Weight.isZero_zero

added theorem LieModule.Weight.zero_apply

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

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

added theorem LieAlgebra.IsKilling.coroot_neg

added theorem LieAlgebra.IsKilling.coroot_zero

added theorem LieModule.Weight.IsNonZero.neg

added theorem LieModule.Weight.IsZero.neg

added theorem LieModule.Weight.coe_neg

added theorem LieModule.Weight.isNonZero_neg

added theorem LieModule.Weight.isZero_neg

added theorem LieModule.Weight.toLinear_neg