Commit 2024-02-13 14:05 398ea8dd

feat(LinearAlgebra/RootSystem/Basic): rm finiteness from def (#10473) There are many interesting infinite root systems, so we remove the finiteness assumption from the definition. A few results use finiteness unnecessarily, so their proofs are revised.