Theorem Submodule.finrank_span_eq_finrank_span

Modification history

2026-01-15 19:06
Mathlib/LinearAlgebra/Span/TensorProduct.lean
feat: the rank of the ℤ-span of the roots of a root system is the dimension (#33846) …
Added Submodule.finrank_span_eq_finrank_spanView on Github →