Commit 2025-04-15 16:58 595daf8e

View on Github →

feat: definition + basic results for chains / strings in root pairings (#24077)

Estimated changes

Modified Mathlib.lean

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

Modified Mathlib/Analysis/Convex/Segment.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

deleted theorem LinearIndependent.linear_combination_pair_of_det_ne_zero

added theorem LinearIndependent.pair_add_smul_add_smul_iff

added theorem LinearIndependent.pair_add_smul_left_iff

added theorem LinearIndependent.pair_add_smul_right_iff

modified theorem LinearIndependent.pair_iff

added theorem LinearIndependent.pair_neg_left_iff

added theorem LinearIndependent.pair_neg_right_iff

added theorem LinearIndependent.pair_smul_iff

modified theorem LinearIndependent.pair_symm_iff

Modified Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

modified theorem RootPairing.Base.cartanMatrix_mem_of_ne

Created Mathlib/LinearAlgebra/RootSystem/Chain.lean

added def RootPairing.chainBotCoeff

added theorem RootPairing.chainBotCoeff_add_chainTopCoeff_le

added theorem RootPairing.chainBotCoeff_chainTopIdx

added theorem RootPairing.chainBotCoeff_of_not_linInd

added theorem RootPairing.chainBotCoeff_relfection_perm

added theorem RootPairing.chainBotCoeff_sub_chainTopCoeff

added def RootPairing.chainBotIdx

added theorem RootPairing.chainCoeff_chainTopIdx_aux

added def RootPairing.chainTopCoeff

added theorem RootPairing.chainTopCoeff_chainTopIdx

added theorem RootPairing.chainTopCoeff_of_not_linInd

added theorem RootPairing.chainTopCoeff_relfection_perm

added theorem RootPairing.chainTopCoeff_sub_chainBotCoeff

added def RootPairing.chainTopIdx

added theorem RootPairing.root_add_nsmul_mem_range_iff_le_chainTopCoeff

added theorem RootPairing.root_add_zsmul_mem_range_iff

added theorem RootPairing.root_chainBotIdx

added theorem RootPairing.root_chainTopIdx

added theorem RootPairing.root_sub_nsmul_mem_range_iff_le_chainBotCoeff

added theorem RootPairing.root_sub_zsmul_mem_range_iff

added theorem RootPairing.setOf_root_add_zsmul_eq_Icc_of_linInd

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean

Modified Mathlib/Order/Interval/Set/Basic.lean

added theorem Set.Icc_eq_Icc_iff