Commit 2025-02-04 09:36 79ad6ef3

feat: drop ordering assumption in RootPairing.coxeterWeight_mem_set_of_isCrystallographic (#21122) Some of the required changes also allow us to unify (and generalise) the RootPairing.IsAnisotropic instances. The means of obtaining these generalisations is to work with a root pairing with coefficients in R taking values in an ordered subring S (in the sense of RootPairing.IsValuedIn). This allows us to avoid assuming R is ordered, and includes the important case of a crystallographic pairing in characteristic zero. The cost of this is that various definitions and lemmas need to be generalised to allow room for the subring S (implemented using an injective algebra S R structure). In particular the definition RootPairing.IsRootPositive becomes RootPairing.RootPositiveForm and has its API substantially reworked. An alternative approach to the headline result (taken in the informal literature) is to invoke RootPairing.restrictScalarsRat but this only works with field coefficients and does not provide the same unifications. We also repair some doc strings (which did not have fully-qualified names, or had names which had drifted from the code).