Commit 2025-03-20 17:27 61c8f96c

feat: a reduced irreducible finite crystallographic root system has roots of at most two different lengths (#23007) In addition to the headline result we also include the following related changes:

• we promote RootPairing.IsReduced to a typeclass
• we introduce the definition RootPairing.InvariantForm (this allows us to drop ordering assumptions on scalars)