Theorem RootPairing.pairingIn_pairingIn_mem_set_of_isCrystallographic_of_isReduced

feat: a finite crystallographic reduced irreducible root pairing containing two roots with Coxeter weight three is spanned by this pair (#23634)

feat: a reduced irreducible finite crystallographic root system has roots of at most two different lengths (#23007) …