Commit 2025-07-17 18:28 5e820da5

feat: add root system induction principle equivalent to connectedness of Dynkin diagram (#26965) The headline result is RootPairing.Base.induction_on_cartanMatrix. In order to prove this we add a second induction principle for root system bases RootPairing.Base.induction_reflect. This is essentially equivalent to the fact that the Weyl group is generated by simple reflections. This is almost the first time RootPairing.Base has been used in a non-trivial way and as a result some further development of its API was necessary. In particular:

• We systematically change pattern ∑ j, f j • P.root j to ∑ j ∈ b.support, f j • P.root j (removing various issues assocated with Fintype ι).
• We introduce a new definition RootPairing.Base.height and use it to redefine RootPairing.Base.IsPos