Commit 2026-01-15 19:06 2f3db78b

feat: the rank of the ℤ-span of the roots of a root system is the dimension (#33846) Essentially all the work goes into proving the key lemma Submodule.finrank_span_eq_finrank_span. This key assumption is that the algebra map R → A is a flat epimorphism. In the actual application R = ℤ and A = ℚ, and a much shorter direct proof is possible but this seemed like a good time to develop the general theory a bit more.