Commit 2025-06-02 06:39 0298271b

View on Github →

feat: various lemmas to support construction of Lie algebra from root system (#25214)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

added theorem Finset.prod_eq_ite

Modified Mathlib/Algebra/Lie/Basic.lean

added theorem LieEquiv.coe_coe

Modified Mathlib/Algebra/Lie/Matrix.lean

added theorem LieModule.toEnd_matrix

modified def Matrix.lieConj

modified theorem Matrix.lieConj_apply

modified theorem Matrix.lieConj_symm_apply

added theorem Matrix.lie_apply

modified def Matrix.reindexLieEquiv

modified theorem Matrix.reindexLieEquiv_apply

modified theorem Matrix.reindexLieEquiv_symm

Modified Mathlib/Algebra/Lie/OfAssociative.lean

Modified Mathlib/Data/Matrix/Diagonal.lean

added theorem Matrix.natCast_apply

added theorem Matrix.ofNat_apply

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

added theorem LinearIndependent.pair_add_left_iff

added theorem LinearIndependent.pair_add_right_iff

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

added theorem RootPairing.Base.toCoweightBasis_repr_coroot

added theorem RootPairing.Base.toWeightBasis_repr_root

Modified Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

added theorem RootPairing.Base.abs_cartanMatrix_apply

added theorem RootPairing.Base.cartanMatrix_map_abs

Modified Mathlib/LinearAlgebra/RootSystem/Chain.lean

added theorem RootPairing.Iic_chainBotCoeff_eq

added theorem RootPairing.Iic_chainTopCoeff_eq

added theorem RootPairing.chainBotCoeff_eq_sSup

added theorem RootPairing.chainBotCoeff_eq_zero_iff

added theorem RootPairing.chainBotCoeff_of_add

added theorem RootPairing.chainTopCoeff_eq_sSup

added theorem RootPairing.chainTopCoeff_eq_zero_iff

added theorem RootPairing.chainTopCoeff_of_sub

added theorem RootPairing.coe_chainBotCoeff_eq_sSup

added theorem RootPairing.coe_chainTopCoeff_eq_sSup

added theorem RootPairing.setOf_root_add_zsmul_mem_eq_Icc

added theorem RootPairing.setOf_root_sub_zsmul_mem_eq_Icc

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.ne_neg