Commit 2026-07-14 19:17 056733e1

View on Github →

chore(LinearAlgebra/Dimension/Torsion/Finite): a torsion module has rank zero (#41739) Also put rank_eq_zero_iff_isTorsion in the Module namespace.

Estimated changes