Commit 2025-02-26 10:06 514991a1
View on Github →feat: more structural lemmas about root pairings (#22213) The main results are:
RootPairing.Base.cartanMatrix_le_zero_of_ne
(off-diagonal entries of Cartan matrices are non-positive)RootPairing.Base.root_sub_root_mem_of_mem_of_mem
(lemma 2.5 from Geck 2017)