Commit 2024-05-28 13:39 53138857

View on Github →

feat(Algebra/Lie/Weights): The root system of a lie algebra. (#13307)

Estimated changes

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

added theorem LieAlgebra.IsKilling.chainBotCoeff_zero_right

added theorem LieAlgebra.IsKilling.chainLength_zero

added theorem LieAlgebra.IsKilling.chainLength_zero_right

added theorem LieAlgebra.IsKilling.chainTopCoeff_zero_right

added theorem LieAlgebra.IsKilling.eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul

added theorem LieAlgebra.IsKilling.eq_neg_or_eq_of_eq_smul

added theorem LieAlgebra.IsKilling.isCrystallographic_rootSystem

added theorem LieAlgebra.IsKilling.isReduced_rootSystem

added def LieAlgebra.IsKilling.reflectRoot

added theorem LieAlgebra.IsKilling.reflectRoot_isNonZero

added theorem LieAlgebra.IsKilling.rootSpace_one_div_two_smul

added theorem LieAlgebra.IsKilling.rootSpace_two_smul

added def LieAlgebra.IsKilling.rootSystem

added theorem LieAlgebra.IsKilling.rootSystem_coroot_apply

added theorem LieAlgebra.IsKilling.rootSystem_pairing_apply

added theorem LieAlgebra.IsKilling.rootSystem_root_apply

added theorem LieAlgebra.IsKilling.rootSystem_toLin_apply

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

added theorem LinearIndependent.pair_iff'