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)

Estimated changes