Commit 2025-05-06 14:17 0da9417a

View on Github →

feat: add Geck's final root system lemma for implementing Lusztig construction (#24263) This proves the lemma in all cases except for 𝔤₂ which will be handled in subsequent work.

Estimated changes

Modified Mathlib/LinearAlgebra/RootSystem/Chain.lean

added theorem RootPairing.chainBotCoeff_if_one_zero

added theorem RootPairing.chainBotCoeff_mul_chainTopCoeff.aux_0

added theorem RootPairing.chainBotCoeff_mul_chainTopCoeff

added theorem RootPairing.chainTopCoeff_if_one_zero

added theorem RootPairing.one_le_chainBotCoeff_of_root_add_mem

added theorem RootPairing.one_le_chainTopCoeff_of_root_add_mem

added theorem RootPairing.pairingIn_le_zero_of_root_add_mem

added theorem RootPairing.zero_le_pairingIn_of_root_sub_mem

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

Modified Mathlib/LinearAlgebra/RootSystem/Reduced.lean

added theorem RootPairing.linearIndependent_of_add_mem_range_root'

added theorem RootPairing.linearIndependent_of_sub_mem_range_root'