feat(Combinatorics): add classification of root systems

[ocfnash]

No description provided.

[kim-em]

Sounds good to me. I expect this will be done easily and soon, but it's a nice statement to have in.

[kim-em]

🤖 Claude says:

The note about [Nonempty ι] isn't right: ι can't be empty here, so the CartanMatrix.A 0 case never arises.

IsRootSystem on its own does permit empty ι, with M = 0. What rules it out is IsIrreducible, which bundles Nontrivial M (Mathlib/LinearAlgebra/RootSystem/Irreducible.lean:148-150). Together with span K (range P.root) = ⊤, an empty ι would give ⊤ = span ∅ = ⊥, contradicting nontriviality. So b.support is nonempty too.

Suggested rewording:

Note that we do not assume `[Nonempty ι]`: it already follows, since `[P.IsIrreducible]`
gives `Nontrivial M` while `[P.IsRootSystem]` makes the roots span `M`.

[kim-em]

Otherwise, looks good to me. Ping me if you agree with the nonempty issue, and i"ll merge.

[ocfnash]

Sounds good to me. I expect this will be done easily and soon, but it's a nice statement to have in.

Thanks, yes I expect this to be crushed easily.