17.2. Properties of root systems and root data
Mathlib contains API for numerous properties of root systems including:
-
Being reduced
RootPairing.IsReduced -
Being irreducible
RootPairing.IsIrreducible -
Being crystallographic
RootPairing.IsCrystallographic
In addition the following concepts also all exist:
-
Morphisms
RootPairing.Hom -
Equivalences
RootPairing.Equiv -
The induced bilinear form
RootPairing.RootForm -
The Weyl group
RootPairing.weylGroup -
The concept of a base
RootPairing.Base(aka a system of simple roots).