Commit 2024-08-10 20:14 0077925c
View on Github →feat (LinearAlgebra/RootSystem) : infinitely many roots when two are parallel (#15582) This PR has a proof that if two roots are linearly independent and "parallel" (meaning their pairings multiply to 4), then the root system containing them is infinite. This is mostly done by refactoring an existing proof.